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	syl5eq	|- ( A e. V -> ran { <. A , B >. } = { B } )