Theorem opex

Description: An ordered pair of classes is a set. Exercise 7 of TakeutiZaring p. 16. (Contributed by NM, 18-Aug-1993) (Revised by Mario Carneiro, 26-Apr-2015) Avoid ax-nul . (Revised by GG, 6-Mar-2026)

	Ref	Expression
Assertion	opex	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V

Proof

Step	Hyp	Ref	Expression
1		df-op	⊢ ⟨ 𝐴 , 𝐵 ⟩ = { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) }
2		simp3	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) → 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } )
3		prex	⊢ { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ V
4	2 3	abex	⊢ { 𝑥 ∣ ( 𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ { { 𝐴 } , { 𝐴 , 𝐵 } } ) } ∈ V
5	1 4	eqeltri	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V