Theorem op1std

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

	Ref	Expression
Hypotheses	op1st.1	|- A e. _V
	op1st.2	|- B e. _V
Assertion	op1std	|- ( C = <. A , B >. -> ( 1st ` C ) = A )

Proof

Step	Hyp	Ref	Expression
1		op1st.1	|- A e. _V
2		op1st.2	|- B e. _V
3		fveq2	|- ( C = <. A , B >. -> ( 1st ` C ) = ( 1st ` <. A , B >. ) )
4	1 2	op1st	|- ( 1st ` <. A , B >. ) = A
5	3 4	eqtrdi	|- ( C = <. A , B >. -> ( 1st ` C ) = A )