# Metamath Proof Explorer

## 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\}$