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\in \mathrm{V}$$
Assertion	rnsnop	$$⊢\mathrm{ran}\left\{⟨A,B⟩\right\}=\left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnvsn.1	$$⊢A\in \mathrm{V}$$
2		rnsnopg	$$⊢A\in \mathrm{V}\to \mathrm{ran}\left\{⟨A,B⟩\right\}=\left\{B\right\}$$
3	1 2	ax-mp	$$⊢\mathrm{ran}\left\{⟨A,B⟩\right\}=\left\{B\right\}$$