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