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 e. _V
Assertion	rnsnop	|- ran { <. A , B >. } = { B }

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	|- A e. _V
2		rnsnopg	|- ( A e. _V -> ran { <. A , B >. } = { B } )
3	1 2	ax-mp	|- ran { <. A , B >. } = { B }