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 V ran A B = B

Proof

Step Hyp Ref Expression
1 df-rn ran A B = dom A B -1
2 dfdm4 dom B A = ran B A -1
3 df-rn ran B A -1 = dom B A -1 -1
4 cnvcnvsn B A -1 -1 = A B -1
5 4 dmeqi dom B A -1 -1 = dom A B -1
6 2 3 5 3eqtri dom B A = dom A B -1
7 1 6 eqtr4i ran A B = dom B A
8 dmsnopg A V dom B A = B
9 7 8 syl5eq A V ran A B = B