Theorem 2ndval2

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

	Ref	Expression
Assertion	2ndval2	|- ( A e. ( _V X. _V ) -> ( 2nd ` 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	op2nd	|- ( 2nd ` <. x , y >. ) = y
5	2 3	op2ndb	|- |^| |^| |^| `' { <. x , y >. } = y
6	4 5	eqtr4i	|- ( 2nd ` <. x , y >. ) = |^| |^| |^| `' { <. x , y >. }
7		fveq2	|- ( A = <. x , y >. -> ( 2nd ` A ) = ( 2nd ` <. x , y >. ) )
8		sneq	|- ( A = <. x , y >. -> { A } = { <. x , y >. } )
9	8	cnveqd	|- ( A = <. x , y >. -> `' { A } = `' { <. x , y >. } )
10	9	inteqd	|- ( A = <. x , y >. -> |^| `' { A } = |^| `' { <. x , y >. } )
11	10	inteqd	|- ( A = <. x , y >. -> |^| |^| `' { A } = |^| |^| `' { <. x , y >. } )
12	11	inteqd	|- ( A = <. x , y >. -> |^| |^| |^| `' { A } = |^| |^| |^| `' { <. x , y >. } )
13	6 7 12	3eqtr4a	|- ( A = <. x , y >. -> ( 2nd ` A ) = |^| |^| |^| `' { A } )
14	13	exlimivv	|- ( E. x E. y A = <. x , y >. -> ( 2nd ` A ) = |^| |^| |^| `' { A } )
15	1 14	sylbi	|- ( A e. ( _V X. _V ) -> ( 2nd ` A ) = |^| |^| |^| `' { A } )