Theorem unielrel

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

	Ref	Expression
Assertion	unielrel	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∪ 𝐴 ∈ ∪ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		elrel	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2		simpr	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → 𝐴 ∈ 𝑅 )
3		vex	⊢ 𝑥 ∈ V
4		vex	⊢ 𝑦 ∈ V
5	3 4	uniopel	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ∪ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑅 )
6	5	a1i	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 → ∪ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑅 ) )
7		eleq1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝑅 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝑅 ) )
8		unieq	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ 𝐴 = ∪ ⟨ 𝑥 , 𝑦 ⟩ )
9	8	eleq1d	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∪ 𝐴 ∈ ∪ 𝑅 ↔ ∪ ⟨ 𝑥 , 𝑦 ⟩ ∈ ∪ 𝑅 ) )
10	6 7 9	3imtr4d	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝑅 → ∪ 𝐴 ∈ ∪ 𝑅 ) )
11	10	exlimivv	⊢ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ∈ 𝑅 → ∪ 𝐴 ∈ ∪ 𝑅 ) )
12	1 2 11	sylc	⊢ ( ( Rel 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∪ 𝐴 ∈ ∪ 𝑅 )