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

Metamath Proof Explorer

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)

Ref Expression
Assertion opex ⊢ 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