Metamath Proof Explorer

Theorem rnsnop

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, 26-Apr-2015)

Ref Expression
Hypothesis cnvsn.1 A V
Assertion rnsnop ran A B = B


Step Hyp Ref Expression
1 cnvsn.1 A V
2 rnsnopg A V ran A B = B
3 1 2 ax-mp ran A B = B