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

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}\left\{⟨A,B⟩\right\}=\mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}$$
2		dfdm4	$$⊢\mathrm{dom}\left\{⟨B,A⟩\right\}=\mathrm{ran}{\left\{⟨B,A⟩\right\}}^{-1}$$
3		df-rn	$$⊢\mathrm{ran}{\left\{⟨B,A⟩\right\}}^{-1}=\mathrm{dom}{{\left\{⟨B,A⟩\right\}}^{-1}}^{-1}$$
4		cnvcnvsn	$$⊢{{\left\{⟨B,A⟩\right\}}^{-1}}^{-1}={\left\{⟨A,B⟩\right\}}^{-1}$$
5	4	dmeqi	$$⊢\mathrm{dom}{{\left\{⟨B,A⟩\right\}}^{-1}}^{-1}=\mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}$$
6	2 3 5	3eqtri	$$⊢\mathrm{dom}\left\{⟨B,A⟩\right\}=\mathrm{dom}{\left\{⟨A,B⟩\right\}}^{-1}$$
7	1 6	eqtr4i	$$⊢\mathrm{ran}\left\{⟨A,B⟩\right\}=\mathrm{dom}\left\{⟨B,A⟩\right\}$$
8		dmsnopg	$$⊢A\in V\to \mathrm{dom}\left\{⟨B,A⟩\right\}=\left\{B\right\}$$
9	7 8	syl5eq	$$⊢A\in V\to \mathrm{ran}\left\{⟨A,B⟩\right\}=\left\{B\right\}$$