Theorem prex 5396

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 5260 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 5395	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5256	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2754	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3455	. . . . . . . 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 3470	1 ⊢ {𝐴, 𝐵} ∈ V

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

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 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  snex  5397  prelpw  5414  opex  5432  opexOLD  5433  elopg  5435  opi2  5438  op1stb  5440  opth  5445  opeqsng  5475  opeqpr  5477  opthwiener  5487  uniop  5488  opthhausdorff  5490  opthhausdorff0  5491  fr2nr  5628  xpsspw  5787  relop  5828  f1prex  7284  unexg  7749  tpex  7751  2oex  8472  en2prd  9059  pw2f1olem  9084  dif1en  9161  opthreg  9603  djuexALT  9984  dfac2b  10190  intwun  10801  wunex2  10804  wuncval2  10813  intgru  10880  xrex  13096  seqexw  14140  pr2pwpr  14604  wwlktovfo  15091  prmreclem2  17075  prdsval  17606  xpsfval  17718  xpssca  17728  xpsvsca  17729  isposix  18478  clatl  18662  ipoval  18684  mgm0b  18815  frmdval  19027  mgmnsgrpex  19110  sgrpnmndex  19111  degenmgmbas  19115  degenmgm2  19120  symg2bas  19587  pmtrprfval  19681  pmtrprfvalrn  19682  psgnprfval1  19716  psgnprfval2  19717  isnzr2hash  20750  psgnghm  21866  psgnco  21869  evpmodpmf1o  21882  mdetralt  22903  m2detleiblem5  22920  m2detleiblem6  22921  m2detleiblem3  22924  m2detleiblem4  22925  m2detleib  22926  indistopon  23299  pptbas  23306  indistpsALT  23311  tuslem  24565  tmslem  24781  ehl2eudis  25723  sqff1o  27491  dchrval  27543  elno  27985  eengv  29539  structvtxvallem  29580  structiedg0val  29582  upgrbi  29653  umgrbi  29661  upgr1e  29673  umgredg  29698  uspgr1e  29807  usgr1e  29808  uspgr1ewop  29811  uspgr2v1e2w  29814  usgr2v1e2w  29815  usgrexmplef  29822  usgrexmpledg  29825  1loopgrnb0  30065  1egrvtxdg1  30072  1egrvtxdg0  30074  umgr2v2evtx  30084  umgr2v2eiedg  30086  umgr2v2e  30088  umgr2v2enb1  30089  umgr2v2evd2  30090  vdegp1ai  30099  vdegp1bi  30100  wlk2v2elem2  30739  wlk2v2e  30740  eupth2lems  30821  frcond2  30850  frcond3  30852  nfrgr2v  30855  frgr3vlem1  30856  frgr3vlem2  30857  frgrncvvdeqlem2  30883  ex-uni  31009  ex-eprel  31016  indf1ofs  33415  idlsrgval  34017  constr0  34351  prsiga  34745  measssd  34830  carsgsigalem  34930  carsgclctun  34936  pmeasmono  34939  eulerpartlemn  34996  probun  35034  coinflipprob  35095  coinflipspace  35096  coinfliprv  35098  coinflippv  35099  cusgredgex  35875  subfacp1lem3  35916  subfacp1lem5  35918  ex-sategoelel12  36161  altopex  36695  altopthsn  36696  altxpsspw  36712  bj-endval  38204  poimirlem9  38515  poimirlem15  38521  impprop  38612  tgrpset  41770  hlhilset  42959  aprilfools2025  43639  kelac2lem  44024  kelac2  44025  mendval  44139  tr3dom  44487  fvrcllb0d  44652  fvrcllb0da  44653  fvrcllb1d  44654  corclrcl  44666  corcltrcl  44698  cotrclrcl  44701  clsk1indlem2  45001  clsk1indlem3  45002  clsk1indlem4  45003  clsk1indlem1  45004  mnuprdlem3  45217  mnurndlem1  45224  permaxpr  45952  prsal  47272  sge0pr  47348  elsprel  48501  sprvalpw  48506  prprvalpw  48541  sbcpr  48547  nnsum3primes4  48830  nnsum3primesgbe  48834  opstrgric  48968  stgrfv  48995  stgredgel  48999  usgrexmpl1lem  49063  usgrexmpl1edg  49066  usgrexmpl1tri  49067  usgrexmpl2lem  49068  usgrexmpl2edg  49071  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2nb4  49077  usgrexmpl2nb5  49078  usgrexmpl2trifr  49079  gpgov  49084  gpgvtx  49085  gpgiedg  49086  gpgiedgdmellem  49088  gpgprismgr4cycllem2  49138  gpgprismgr4cycllem3  49139  gpgprismgr4cycllem8  49144  gpgprismgr4cycllem10  49146  pgnbgreunbgr  49167  fprmappr  49401  zlmodzxzlmod  49410  zlmodzxzel  49411  zlmodzxz0  49412  zlmodzxzscm  49413  zlmodzxzadd  49414  zlmodzxzldeplem1  49556  zlmodzxzldeplem3  49558  zlmodzxzldeplem4  49559  ldepsnlinclem1  49561  ldepsnlinclem2  49562  ldepsnlinc  49564  2arymaptfo  49710  prelrrx2  49769  rrx2xpref1o  49774  rrx2plordisom  49779  ehl2eudisval0  49781  rrx2linesl  49799  2sphere0  49806  line2  49808  line2x  49810  line2y  49811  resipos  50027  fucoppcffth  50463  termc2  50570  uobeqterm  50598  incat  50653  onsetreclem1  50742