This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑅 ∧ 𝐴 ∈ 𝑅 ) → ∪ 𝐴 ∈ ∪ 𝑅 )