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