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

Metamath Proof Explorer

Theorem prex

Description: The Axiom of Pairing using class variables. Theorem 7.13 of Quine p. 51. By virtue of its definition, an unordered pair remains a set (even though no longer a pair) even when its components are proper classes (see prprc ), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993) Avoid ax-nul and shorten proof. (Revised by GG, 6-Mar-2026)

Ref Expression
Assertion prex 
|- { A , B } e. _V

Proof

Step Hyp Ref Expression
1 axprg 
 |-  E. z A. w ( ( w = A \/ w = B ) -> w e. z )
2 1 sepexi 
 |-  E. z A. w ( w e. z <-> ( w = A \/ w = B ) )
3 dfcleq 
 |-  ( z = { A , B } <-> A. w ( w e. z <-> w e. { A , B } ) )
4 vex 
 |-  w e. _V
5 4 elpr 
 |-  ( w e. { A , B } <-> ( w = A \/ w = B ) )
6 5 bibi2i 
 |-  ( ( w e. z <-> w e. { A , B } ) <-> ( w e. z <-> ( w = A \/ w = B ) ) )
7 6 albii 
 |-  ( A. w ( w e. z <-> w e. { A , B } ) <-> A. w ( w e. z <-> ( w = A \/ w = B ) ) )
8 3 7 bitri 
 |-  ( z = { A , B } <-> A. w ( w e. z <-> ( w = A \/ w = B ) ) )
9 8 exbii 
 |-  ( E. z z = { A , B } <-> E. z A. w ( w e. z <-> ( w = A \/ w = B ) ) )
10 2 9 mpbir 
 |-  E. z z = { A , B }
11 10 issetri 
 |-  { A , B } e. _V