Theorem prex 5401

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 4728), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5264 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 5400	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5260	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2756	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3458	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4609	. . . . . . 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 3473	1 ⊢ {𝐴, 𝐵} ∈ V

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  snex  5402  prelpw  5419  opex  5437  opexOLD  5438  elopg  5440  opi2  5443  op1stb  5445  opth  5450  opeqsng  5480  opeqpr  5482  opthwiener  5492  uniop  5493  opthhausdorff  5495  opthhausdorff0  5496  fr2nr  5633  xpsspw  5793  relop  5835  f1prex  7318  unexg  7787  tpex  7789  2oex  8519  en2prd  9106  pw2f1olem  9131  dif1en  9208  opthreg  9649  djuexALT  10033  dfac2b  10239  intwun  10850  wunex2  10853  wuncval2  10862  intgru  10929  xrex  13145  seqexw  14190  pr2pwpr  14654  wwlktovfo  15143  prmreclem2  17127  prdsval  17658  xpsfval  17770  xpssca  17780  xpsvsca  17781  isposix  18530  clatl  18714  ipoval  18736  mgm0b  18867  frmdval  19079  mgmnsgrpex  19162  sgrpnmndex  19163  degenmgmbas  19167  degenmgm2  19172  symg2bas  19640  pmtrprfval  19734  pmtrprfvalrn  19735  psgnprfval1  19769  psgnprfval2  19770  isnzr2hash  20803  psgnghm  21919  psgnco  21922  evpmodpmf1o  21935  mdetralt  22956  m2detleiblem5  22973  m2detleiblem6  22974  m2detleiblem3  22977  m2detleiblem4  22978  m2detleib  22979  indistopon  23352  pptbas  23359  indistpsALT  23364  tuslem  24618  tmslem  24834  ehl2eudis  25776  sqff1o  27542  dchrval  27594  elno  28036  eengv  29590  structvtxvallem  29631  structiedg0val  29633  upgrbi  29704  umgrbi  29712  upgr1e  29724  umgredg  29749  uspgr1e  29858  usgr1e  29859  uspgr1ewop  29862  uspgr2v1e2w  29865  usgr2v1e2w  29866  usgrexmplef  29873  usgrexmpledg  29876  1loopgrnb0  30116  1egrvtxdg1  30123  1egrvtxdg0  30125  umgr2v2evtx  30135  umgr2v2eiedg  30137  umgr2v2e  30139  umgr2v2enb1  30140  umgr2v2evd2  30141  vdegp1ai  30150  vdegp1bi  30151  wlk2v2elem2  30790  wlk2v2e  30791  eupth2lems  30872  frcond2  30901  frcond3  30903  nfrgr2v  30906  frgr3vlem1  30907  frgr3vlem2  30908  frgrncvvdeqlem2  30934  ex-uni  31060  ex-eprel  31067  indf1ofs  33506  idlsrgval  34119  constr0  34452  prsiga  34846  measssd  34931  carsgsigalem  35030  carsgclctun  35036  pmeasmono  35039  eulerpartlemn  35096  probun  35134  coinflipprob  35195  coinflipspace  35196  coinfliprv  35198  coinflippv  35199  gdlop1fv  35976  cusgredgex  36076  subfacp1lem3  36127  subfacp1lem5  36129  ex-sategoelel12  36372  altopex  36916  altopthsn  36917  altxpsspw  36933  bj-endval  38441  poimirlem9  38752  poimirlem15  38758  impprop  38849  tgrpset  42005  hlhilset  43194  aprilfools2025  43889  kelac2lem  44270  kelac2  44271  mendval  44384  tr3dom  44732  fvrcllb0d  44896  fvrcllb0da  44897  fvrcllb1d  44898  corclrcl  44910  corcltrcl  44942  cotrclrcl  44945  clsk1indlem2  45245  clsk1indlem3  45246  clsk1indlem4  45247  clsk1indlem1  45248  mnuprdlem3  45461  mnurndlem1  45468  permaxpr  46206  prsal  47543  sge0pr  47619  elsprel  48772  sprvalpw  48777  prprvalpw  48812  sbcpr  48818  nnsum3primes4  49101  nnsum3primesgbe  49105  opstrgric  49239  stgrfv  49266  stgredgel  49270  usgrexmpl1lem  49334  usgrexmpl1edg  49337  usgrexmpl1tri  49338  usgrexmpl2lem  49339  usgrexmpl2edg  49342  usgrexmpl2nb0  49344  usgrexmpl2nb1  49345  usgrexmpl2nb2  49346  usgrexmpl2nb3  49347  usgrexmpl2nb4  49348  usgrexmpl2nb5  49349  usgrexmpl2trifr  49350  gpgov  49355  gpgvtx  49356  gpgiedg  49357  gpgiedgdmellem  49359  gpgprismgr4cycllem2  49409  gpgprismgr4cycllem3  49410  gpgprismgr4cycllem8  49415  gpgprismgr4cycllem10  49417  pgnbgreunbgr  49438  fprmappr  49672  zlmodzxzlmod  49681  zlmodzxzel  49682  zlmodzxz0  49683  zlmodzxzscm  49684  zlmodzxzadd  49685  zlmodzxzldeplem1  49827  zlmodzxzldeplem3  49829  zlmodzxzldeplem4  49830  ldepsnlinclem1  49832  ldepsnlinclem2  49833  ldepsnlinc  49835  2arymaptfo  49981  resipos  50304  fucoppcffth  50761  termc2  50868  uobeqterm  50899  incat  50954  onsetreclem1  51088