Metamath Proof Explorer

Theorem ex-cnv

Description: Example for df-cnv . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion ex-cnv 
|- `' { <. 2 , 6 >. , <. 3 , 9 >. } = { <. 6 , 2 >. , <. 9 , 3 >. }

Proof

Step Hyp Ref Expression
1 cnvun 
 |-  `' ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } ) = ( `' { <. 2 , 6 >. } u. `' { <. 3 , 9 >. } )
2 2nn 
 |-  2 e. NN
3 2 elexi 
 |-  2 e. _V
4 6nn 
 |-  6 e. NN
5 4 elexi 
 |-  6 e. _V
6 3 5 cnvsn 
 |-  `' { <. 2 , 6 >. } = { <. 6 , 2 >. }
7 3nn 
 |-  3 e. NN
8 7 elexi 
 |-  3 e. _V
9 9nn 
 |-  9 e. NN
10 9 elexi 
 |-  9 e. _V
11 8 10 cnvsn 
 |-  `' { <. 3 , 9 >. } = { <. 9 , 3 >. }
12 6 11 uneq12i 
 |-  ( `' { <. 2 , 6 >. } u. `' { <. 3 , 9 >. } ) = ( { <. 6 , 2 >. } u. { <. 9 , 3 >. } )
13 1 12 eqtri 
 |-  `' ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } ) = ( { <. 6 , 2 >. } u. { <. 9 , 3 >. } )
14 df-pr 
 |-  { <. 2 , 6 >. , <. 3 , 9 >. } = ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } )
15 14 cnveqi 
 |-  `' { <. 2 , 6 >. , <. 3 , 9 >. } = `' ( { <. 2 , 6 >. } u. { <. 3 , 9 >. } )
16 df-pr 
 |-  { <. 6 , 2 >. , <. 9 , 3 >. } = ( { <. 6 , 2 >. } u. { <. 9 , 3 >. } )
17 13 15 16 3eqtr4i 
 |-  `' { <. 2 , 6 >. , <. 3 , 9 >. } = { <. 6 , 2 >. , <. 9 , 3 >. }