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

Metamath Proof Explorer

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 ⊢ A B ∈ V

Proof

Step Hyp Ref Expression
1 dfopif ⊢ A B = if A ∈ V ∧ B ∈ V A A B ∅
2 prex ⊢ A A B ∈ V
3 0ex ⊢ ∅ ∈ V
4 2 3 ifex ⊢ if A ∈ V ∧ B ∈ V A A B ∅ ∈ V
5 1 4 eqeltri ⊢ A B ∈ V