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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐶 , 𝐷 } )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
2	1	rneqi	⊢ ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } )
3		rnsnopg	⊢ ( 𝐴 ∈ 𝑉 → ran { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐶 } )
4	3	adantr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐴 , 𝐶 ⟩ } = { 𝐶 } )
5		rnsnopg	⊢ ( 𝐵 ∈ 𝑊 → ran { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐷 } )
6	5	adantl	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐷 } )
7	4 6	uneq12d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( { 𝐶 } ∪ { 𝐷 } ) )
8		rnun	⊢ ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = ( ran { ⟨ 𝐴 , 𝐶 ⟩ } ∪ ran { ⟨ 𝐵 , 𝐷 ⟩ } )
9		df-pr	⊢ { 𝐶 , 𝐷 } = ( { 𝐶 } ∪ { 𝐷 } )
10	7 8 9	3eqtr4g	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran ( { ⟨ 𝐴 , 𝐶 ⟩ } ∪ { ⟨ 𝐵 , 𝐷 ⟩ } ) = { 𝐶 , 𝐷 } )
11	2 10	syl5eq	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ran { ⟨ 𝐴 , 𝐶 ⟩ , ⟨ 𝐵 , 𝐷 ⟩ } = { 𝐶 , 𝐷 } )