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

Metamath Proof Explorer

Theorem rnsnopg

Description: The range of a singleton of an ordered pair is the singleton of the second member. (Contributed by NM, 24-Jul-2004) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion rnsnopg 
|- ( A e. V -> ran { <. A , B >. } = { B } )

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran { <. A , B >. } = dom `' { <. A , B >. }
2 dfdm4 
 |-  dom { <. B , A >. } = ran `' { <. B , A >. }
3 df-rn 
 |-  ran `' { <. B , A >. } = dom `' `' { <. B , A >. }
4 cnvcnvsn 
 |-  `' `' { <. B , A >. } = `' { <. A , B >. }
5 4 dmeqi 
 |-  dom `' `' { <. B , A >. } = dom `' { <. A , B >. }
6 2 3 5 3eqtri 
 |-  dom { <. B , A >. } = dom `' { <. A , B >. }
7 1 6 eqtr4i 
 |-  ran { <. A , B >. } = dom { <. B , A >. }
8 dmsnopg 
 |-  ( A e. V -> dom { <. B , A >. } = { B } )
9 7 8 eqtrid 
 |-  ( A e. V -> ran { <. A , B >. } = { B } )