Theorem op1st

Description: Extract the first member of an ordered pair. (Contributed by NM, 5-Oct-2004)

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

Proof

Step	Hyp	Ref	Expression
1		op1st.1	|- A e. _V
2		op1st.2	|- B e. _V
3		1stval	|- ( 1st ` <. A , B >. ) = U. dom { <. A , B >. }
4	1 2	op1sta	|- U. dom { <. A , B >. } = A
5	3 4	eqtri	|- ( 1st ` <. A , B >. ) = A