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


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