Theorem prex 5407

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 4731), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5267 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 5406	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5262	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2755	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3457	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4612	. . . . . . 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 3472	1 ⊢ {𝐴, 𝐵} ∈ V

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

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 2734  ax-sep 5255  ax-pr 5402

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 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  snex  5408  prelpw  5425  opex  5443  opexOLD  5444  elopg  5446  opi2  5449  op1stb  5451  opth  5456  opeqsng  5484  opeqpr  5486  opthwiener  5495  uniop  5496  opthhausdorff  5498  opthhausdorff0  5499  fr2nr  5636  xpsspw  5794  relop  5834  f1prex  7289  unexg  7749  tpex  7751  2oex  8471  en2prd  9058  pw2f1olem  9083  dif1en  9160  opthreg  9601  djuexALT  9931  dfac2b  10137  intwun  10748  wunex2  10751  wuncval2  10760  intgru  10827  xrex  13041  seqexw  14085  pr2pwpr  14548  wwlktovfo  15035  prmreclem2  17015  prdsval  17546  xpsfval  17658  xpssca  17668  xpsvsca  17669  isposix  18418  clatl  18602  ipoval  18624  mgm0b  18755  frmdval  18966  mgmnsgrpex  19049  sgrpnmndex  19050  degenmgmbas  19054  degenmgm2  19059  symg2bas  19526  pmtrprfval  19620  pmtrprfvalrn  19621  psgnprfval1  19655  psgnprfval2  19656  isnzr2hash  20686  psgnghm  21799  psgnco  21802  evpmodpmf1o  21815  mdetralt  22836  m2detleiblem5  22853  m2detleiblem6  22854  m2detleiblem3  22857  m2detleiblem4  22858  m2detleib  22859  indistopon  23232  pptbas  23239  indistpsALT  23244  tuslem  24498  tmslem  24714  ehl2eudis  25656  sqff1o  27426  dchrval  27478  elno  27890  eengv  29444  structvtxvallem  29485  structiedg0val  29487  upgrbi  29558  umgrbi  29566  upgr1e  29578  umgredg  29603  uspgr1e  29712  usgr1e  29713  uspgr1ewop  29716  uspgr2v1e2w  29719  usgr2v1e2w  29720  usgrexmplef  29727  usgrexmpledg  29730  1loopgrnb0  29970  1egrvtxdg1  29977  1egrvtxdg0  29979  umgr2v2evtx  29989  umgr2v2eiedg  29991  umgr2v2e  29993  umgr2v2enb1  29994  umgr2v2evd2  29995  vdegp1ai  30004  vdegp1bi  30005  wlk2v2elem2  30644  wlk2v2e  30645  eupth2lems  30726  frcond2  30755  frcond3  30757  nfrgr2v  30760  frgr3vlem1  30761  frgr3vlem2  30762  frgrncvvdeqlem2  30788  ex-uni  30914  ex-eprel  30921  indf1ofs  33320  idlsrgval  33921  constr0  34255  prsiga  34649  measssd  34734  carsgsigalem  34834  carsgclctun  34840  pmeasmono  34843  eulerpartlemn  34900  probun  34938  coinflipprob  34999  coinflipspace  35000  coinfliprv  35002  coinflippv  35003  cusgredgex  35728  subfacp1lem3  35769  subfacp1lem5  35771  ex-sategoelel12  36014  altopex  36548  altopthsn  36549  altxpsspw  36565  bj-endval  38075  poimirlem9  38386  poimirlem15  38392  tgrpset  41626  hlhilset  42815  aprilfools2025  43528  kelac2lem  43913  kelac2  43914  mendval  44028  tr3dom  44376  fvrcllb0d  44541  fvrcllb0da  44542  fvrcllb1d  44543  corclrcl  44555  corcltrcl  44587  cotrclrcl  44590  clsk1indlem2  44890  clsk1indlem3  44891  clsk1indlem4  44892  clsk1indlem1  44893  mnuprdlem3  45106  mnurndlem1  45113  permaxpr  45841  prsal  47154  sge0pr  47230  elsprel  48383  sprvalpw  48388  prprvalpw  48423  sbcpr  48429  nnsum3primes4  48712  nnsum3primesgbe  48716  opstrgric  48850  stgrfv  48877  stgredgel  48881  usgrexmpl1lem  48945  usgrexmpl1edg  48948  usgrexmpl1tri  48949  usgrexmpl2lem  48950  usgrexmpl2edg  48953  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2nb4  48959  usgrexmpl2nb5  48960  usgrexmpl2trifr  48961  gpgov  48966  gpgvtx  48967  gpgiedg  48968  gpgiedgdmellem  48970  gpgprismgr4cycllem2  49020  gpgprismgr4cycllem3  49021  gpgprismgr4cycllem8  49026  gpgprismgr4cycllem10  49028  pgnbgreunbgr  49049  fprmappr  49283  zlmodzxzlmod  49292  zlmodzxzel  49293  zlmodzxz0  49294  zlmodzxzscm  49295  zlmodzxzadd  49296  zlmodzxzldeplem1  49438  zlmodzxzldeplem3  49440  zlmodzxzldeplem4  49441  ldepsnlinclem1  49443  ldepsnlinclem2  49444  ldepsnlinc  49446  2arymaptfo  49592  prelrrx2  49651  rrx2xpref1o  49656  rrx2plordisom  49661  ehl2eudisval0  49663  rrx2linesl  49681  2sphere0  49688  line2  49690  line2x  49692  line2y  49693  resipos  49909  fucoppcffth  50345  termc2  50452  uobeqterm  50480  incat  50535  onsetreclem1  50639