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	$⊢ (A \in V \land B \in W) \to ran \{⟨A, C⟩, ⟨B, D⟩\} = \{C, D\}$

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

Metamath Proof Explorer