Theorem opexOLD

Description: Obsolete version of opex as of 6-Mar-2026. (Contributed by NM, 18-Aug-1993) (Revised by Mario Carneiro, 26-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		dfopif	⊢ ⟨ 𝐴 , 𝐵 ⟩ = if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ )
2		prex	⊢ { { 𝐴 } , { 𝐴 , 𝐵 } } ∈ V
3		0ex	⊢ ∅ ∈ V
4	2 3	ifex	⊢ if ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) , { { 𝐴 } , { 𝐴 , 𝐵 } } , ∅ ) ∈ V
5	1 4	eqeltri	⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V