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) Avoid ax-nul . (Revised by GG, 6-Mar-2026)

Ref Expression
Assertion opex ⊢ A B ∈ V

Proof

Step Hyp Ref Expression
1 df-op ⊢ A B = x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B
2 simp3 ⊢ A ∈ V ∧ B ∈ V ∧ x ∈ A A B → x ∈ A A B
3 prex ⊢ A A B ∈ V
4 2 3 abex ⊢ x | A ∈ V ∧ B ∈ V ∧ x ∈ A A B ∈ V
5 1 4 eqeltri ⊢ A B ∈ V