This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } )