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

Metamath Proof Explorer

Theorem elvvuni

Description: An ordered pair contains its union. (Contributed by NM, 16-Sep-2006)

Ref Expression
Assertion elvvuni ( 𝐴 ∈ ( V × V ) → ∪ 𝐴 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 elvv ⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
2 vex ⊢ 𝑥 ∈ V
3 vex ⊢ 𝑦 ∈ V
4 2 3 uniop ⊢ ∪ ⟨ 𝑥 , 𝑦 ⟩ = { 𝑥 , 𝑦 }
5 2 3 opi2 ⊢ { 𝑥 , 𝑦 } ∈ ⟨ 𝑥 , 𝑦 ⟩
6 4 5 eqeltri ⊢ ∪ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑥 , 𝑦 ⟩
7 unieq ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ 𝐴 = ∪ ⟨ 𝑥 , 𝑦 ⟩ )
8 id ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
9 7 8 eleq12d ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( ∪ 𝐴 ∈ 𝐴 ↔ ∪ ⟨ 𝑥 , 𝑦 ⟩ ∈ ⟨ 𝑥 , 𝑦 ⟩ ) )
10 6 9 mpbiri ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ 𝐴 ∈ 𝐴 )
11 10 exlimivv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ∪ 𝐴 ∈ 𝐴 )
12 1 11 sylbi ⊢ ( 𝐴 ∈ ( V × V ) → ∪ 𝐴 ∈ 𝐴 )