# Metamath Proof Explorer

## Theorem rnpropg

Description: The range of a pair of ordered pairs is the pair of second members. (Contributed by Thierry Arnoux, 3-Jan-2017)

Ref Expression
Assertion rnpropg ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{ran}\left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}=\left\{{C},{D}\right\}$

### Proof

Step Hyp Ref Expression
1 df-pr ${⊢}\left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}=\left\{⟨{A},{C}⟩\right\}\cup \left\{⟨{B},{D}⟩\right\}$
2 1 rneqi ${⊢}\mathrm{ran}\left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}=\mathrm{ran}\left(\left\{⟨{A},{C}⟩\right\}\cup \left\{⟨{B},{D}⟩\right\}\right)$
3 rnsnopg ${⊢}{A}\in {V}\to \mathrm{ran}\left\{⟨{A},{C}⟩\right\}=\left\{{C}\right\}$
4 3 adantr ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{ran}\left\{⟨{A},{C}⟩\right\}=\left\{{C}\right\}$
5 rnsnopg ${⊢}{B}\in {W}\to \mathrm{ran}\left\{⟨{B},{D}⟩\right\}=\left\{{D}\right\}$
6 5 adantl ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{ran}\left\{⟨{B},{D}⟩\right\}=\left\{{D}\right\}$
7 4 6 uneq12d ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{ran}\left\{⟨{A},{C}⟩\right\}\cup \mathrm{ran}\left\{⟨{B},{D}⟩\right\}=\left\{{C}\right\}\cup \left\{{D}\right\}$
8 rnun ${⊢}\mathrm{ran}\left(\left\{⟨{A},{C}⟩\right\}\cup \left\{⟨{B},{D}⟩\right\}\right)=\mathrm{ran}\left\{⟨{A},{C}⟩\right\}\cup \mathrm{ran}\left\{⟨{B},{D}⟩\right\}$
9 df-pr ${⊢}\left\{{C},{D}\right\}=\left\{{C}\right\}\cup \left\{{D}\right\}$
10 7 8 9 3eqtr4g ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{ran}\left(\left\{⟨{A},{C}⟩\right\}\cup \left\{⟨{B},{D}⟩\right\}\right)=\left\{{C},{D}\right\}$
11 2 10 syl5eq ${⊢}\left({A}\in {V}\wedge {B}\in {W}\right)\to \mathrm{ran}\left\{⟨{A},{C}⟩,⟨{B},{D}⟩\right\}=\left\{{C},{D}\right\}$