Theorem uniopel

Description: Ordered pair membership is inherited by class union. (Contributed by NM, 13-May-2008) (Revised by Mario Carneiro, 26-Apr-2015)

	Ref	Expression
Hypotheses	opthw.1	⊢ 𝐴 ∈ V
	opthw.2	⊢ 𝐵 ∈ V
Assertion	uniopel	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ∪ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		opthw.1	⊢ 𝐴 ∈ V
2		opthw.2	⊢ 𝐵 ∈ V
3	1 2	uniop	⊢ ∪ ⟨ 𝐴 , 𝐵 ⟩ = { 𝐴 , 𝐵 }
4	1 2	opi2	⊢ { 𝐴 , 𝐵 } ∈ ⟨ 𝐴 , 𝐵 ⟩
5	3 4	eqeltri	⊢ ∪ ⟨ 𝐴 , 𝐵 ⟩ ∈ ⟨ 𝐴 , 𝐵 ⟩
6		elssuni	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ⟨ 𝐴 , 𝐵 ⟩ ⊆ ∪ 𝐶 )
7	6	sseld	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ( ∪ ⟨ 𝐴 , 𝐵 ⟩ ∈ ⟨ 𝐴 , 𝐵 ⟩ → ∪ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ 𝐶 ) )
8	5 7	mpi	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ 𝐶 → ∪ ⟨ 𝐴 , 𝐵 ⟩ ∈ ∪ 𝐶 )