Theorem 1stval2

Description: Alternate value of the function that extracts the first member of an ordered pair. Definition 5.13 (i) of Monk1 p. 52. (Contributed by NM, 18-Aug-2006)

	Ref	Expression
Assertion	1stval2	|- ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )

Proof

Step	Hyp	Ref	Expression
1		elvv	|- ( A e. ( _V X. _V ) <-> E. x E. y A = <. x , y >. )
2		vex	|- x e. _V
3		vex	|- y e. _V
4	2 3	op1st	|- ( 1st ` <. x , y >. ) = x
5	2 3	op1stb	|- |^| |^| <. x , y >. = x
6	4 5	eqtr4i	|- ( 1st ` <. x , y >. ) = |^| |^| <. x , y >.
7		fveq2	|- ( A = <. x , y >. -> ( 1st ` A ) = ( 1st ` <. x , y >. ) )
8		inteq	|- ( A = <. x , y >. -> |^| A = |^| <. x , y >. )
9	8	inteqd	|- ( A = <. x , y >. -> |^| |^| A = |^| |^| <. x , y >. )
10	6 7 9	3eqtr4a	|- ( A = <. x , y >. -> ( 1st ` A ) = |^| |^| A )
11	10	exlimivv	|- ( E. x E. y A = <. x , y >. -> ( 1st ` A ) = |^| |^| A )
12	1 11	sylbi	|- ( A e. ( _V X. _V ) -> ( 1st ` A ) = |^| |^| A )