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