Metamath Proof Explorer

Theorem op1std

Description: Extract the first member of an ordered pair. (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses op1st.1 ⊢ A ∈ V
op1st.2 ⊢ B ∈ V
Assertion op1std ⊢ C = A B → 1 st ⁡ C = A

Proof

Step Hyp Ref Expression
1 op1st.1 ⊢ A ∈ V
2 op1st.2 ⊢ B ∈ V
3 fveq2 ⊢ C = A B → 1 st ⁡ C = 1 st ⁡ A B
4 1 2 op1st ⊢ 1 st ⁡ A B = A
5 3 4 eqtrdi ⊢ C = A B → 1 st ⁡ C = A