unielrel

Description: The membership relation for a relation is inherited by class union. (Contributed by NM, 17-Sep-2006)

		Ref	Expression
	Assertion	unielrel	$⊢ (Rel R \land A \in R) \to ⋃ A \in ⋃ R$

Step	Hyp	Ref	Expression
1		elrel	$⊢ (Rel R \land A \in R) \to \exists x \exists y A = ⟨x, y⟩$
2		simpr	$⊢ (Rel R \land A \in R) \to A \in R$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	uniopel	$⊢ ⟨x, y⟩ \in R \to ⋃ ⟨x, y⟩ \in ⋃ R$
6	5	a1i	$⊢ A = ⟨x, y⟩ \to (⟨x, y⟩ \in R \to ⋃ ⟨x, y⟩ \in ⋃ R)$
7		eleq1	$⊢ A = ⟨x, y⟩ \to (A \in R \leftrightarrow ⟨x, y⟩ \in R)$
8		unieq	$⊢ A = ⟨x, y⟩ \to ⋃ A = ⋃ ⟨x, y⟩$
9	8	eleq1d	$⊢ A = ⟨x, y⟩ \to (⋃ A \in ⋃ R \leftrightarrow ⋃ ⟨x, y⟩ \in ⋃ R)$
10	6 7 9	3imtr4d	$⊢ A = ⟨x, y⟩ \to (A \in R \to ⋃ A \in ⋃ R)$
11	10	exlimivv	$⊢ \exists x \exists y A = ⟨x, y⟩ \to (A \in R \to ⋃ A \in ⋃ R)$
12	1 2 11	sylc	$⊢ (Rel R \land A \in R) \to ⋃ A \in ⋃ R$

Metamath Proof Explorer