Theorem prex 5414

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 4738), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5274 and shorten proof. (Revised by GG, 6-Mar-2026.)

Assertion

Ref	Expression
prex	⊢ {𝐴, 𝐵} ∈ V

Proof of Theorem prex

Dummy variables 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axprg 5413	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5269	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2759	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3462	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4619	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 340	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1852	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 278	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1881	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 234	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3477	1 ⊢ {𝐴, 𝐵} ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2146  Vcvv 3458  {cpr 4596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  snex  5415  prelpw  5432  opex  5450  opexOLD  5451  elopg  5453  opi2  5456  op1stb  5458  opth  5463  opeqsng  5491  opeqpr  5493  opthwiener  5502  uniop  5503  opthhausdorff  5505  opthhausdorff0  5506  fr2nr  5643  xpsspw  5801  relop  5841  f1prex  7293  unexg  7754  tpex  7756  2oex  8474  en2prd  9054  pw2f1olem  9079  dif1en  9156  opthreg  9597  djuexALT  9927  dfac2b  10133  intwun  10738  wunex2  10741  wuncval2  10750  intgru  10817  xrex  13029  seqexw  14073  pr2pwpr  14536  wwlktovfo  15021  prmreclem2  17002  prdsval  17533  xpsfval  17645  xpssca  17655  xpsvsca  17656  isposix  18405  clatl  18589  ipoval  18611  mgm0b  18740  frmdval  18941  mgmnsgrpex  19024  sgrpnmndex  19025  symg2bas  19494  pmtrprfval  19588  pmtrprfvalrn  19589  psgnprfval1  19623  psgnprfval2  19624  isnzr2hash  20654  psgnghm  21767  psgnco  21770  evpmodpmf1o  21783  mdetralt  22802  m2detleiblem5  22819  m2detleiblem6  22820  m2detleiblem3  22823  m2detleiblem4  22824  m2detleib  22825  indistopon  23195  pptbas  23202  indistpsALT  23207  tuslem  24460  tmslem  24676  ehl2eudis  25618  sqff1o  27383  dchrval  27435  elno  27847  eengv  29366  structvtxvallem  29407  structiedg0val  29409  upgrbi  29480  umgrbi  29488  upgr1e  29500  umgredg  29525  uspgr1e  29631  usgr1e  29632  uspgr1ewop  29635  uspgr2v1e2w  29638  usgr2v1e2w  29639  usgrexmplef  29646  usgrexmpledg  29649  1loopgrnb0  29889  1egrvtxdg1  29896  1egrvtxdg0  29898  umgr2v2evtx  29908  umgr2v2eiedg  29910  umgr2v2e  29912  umgr2v2enb1  29913  umgr2v2evd2  29914  vdegp1ai  29923  vdegp1bi  29924  wlk2v2elem2  30544  wlk2v2e  30545  eupth2lems  30626  frcond2  30655  frcond3  30657  nfrgr2v  30660  frgr3vlem1  30661  frgr3vlem2  30662  frgrncvvdeqlem2  30688  ex-uni  30814  ex-eprel  30821  indf1ofs  33223  idlsrgval  33824  constr0  34158  prsiga  34552  measssd  34637  carsgsigalem  34737  carsgclctun  34743  pmeasmono  34746  eulerpartlemn  34803  probun  34841  coinflipprob  34902  coinflipspace  34903  coinfliprv  34905  coinflippv  34906  cusgredgex  35635  subfacp1lem3  35695  subfacp1lem5  35697  ex-sategoelel12  35940  altopex  36473  altopthsn  36474  altxpsspw  36490  bj-endval  38000  poimirlem9  38321  poimirlem15  38327  tgrpset  41560  hlhilset  42749  aprilfools2025  43447  kelac2lem  43832  kelac2  43833  mendval  43947  tr3dom  44295  fvrcllb0d  44460  fvrcllb0da  44461  fvrcllb1d  44462  corclrcl  44474  corcltrcl  44506  cotrclrcl  44509  clsk1indlem2  44809  clsk1indlem3  44810  clsk1indlem4  44811  clsk1indlem1  44812  mnuprdlem3  45025  mnurndlem1  45032  permaxpr  45760  prsal  47073  sge0pr  47149  elsprel  48265  sprvalpw  48270  prprvalpw  48305  sbcpr  48311  nnsum3primes4  48594  nnsum3primesgbe  48598  opstrgric  48732  stgrfv  48759  stgredgel  48763  usgrexmpl1lem  48827  usgrexmpl1edg  48830  usgrexmpl1tri  48831  usgrexmpl2lem  48832  usgrexmpl2edg  48835  usgrexmpl2nb0  48837  usgrexmpl2nb1  48838  usgrexmpl2nb2  48839  usgrexmpl2nb3  48840  usgrexmpl2nb4  48841  usgrexmpl2nb5  48842  usgrexmpl2trifr  48843  gpgov  48848  gpgvtx  48849  gpgiedg  48850  gpgiedgdmellem  48852  gpgprismgr4cycllem2  48902  gpgprismgr4cycllem3  48903  gpgprismgr4cycllem8  48908  gpgprismgr4cycllem10  48910  pgnbgreunbgr  48931  fprmappr  49166  zlmodzxzlmod  49175  zlmodzxzel  49176  zlmodzxz0  49177  zlmodzxzscm  49178  zlmodzxzadd  49179  zlmodzxzldeplem1  49321  zlmodzxzldeplem3  49323  zlmodzxzldeplem4  49324  ldepsnlinclem1  49326  ldepsnlinclem2  49327  ldepsnlinc  49329  2arymaptfo  49475  prelrrx2  49534  rrx2xpref1o  49539  rrx2plordisom  49544  ehl2eudisval0  49546  rrx2linesl  49564  2sphere0  49571  line2  49573  line2x  49575  line2y  49576  resipos  49794  fucoppcffth  50230  termc2  50337  uobeqterm  50365  incat  50420  onsetreclem1  50524