Theorem prex 5400

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 4729), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5261 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 5399	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5256	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2758	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3461	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4610	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 340	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1842	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 278	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1871	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 234	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3476	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:   ↔ wb 209   ∨ wo 860  ∀wal 1561   = wceq 1563  ∃wex 1802   ∈ wcel 2145  Vcvv 3457  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  snex  5401  prelpw  5418  opex  5436  opexOLD  5437  elopg  5439  opi2  5442  op1stb  5444  opth  5449  opeqsng  5477  opeqpr  5479  opthwiener  5488  uniop  5489  opthhausdorff  5491  opthhausdorff0  5492  fr2nr  5629  xpsspw  5787  relop  5827  f1prex  7272  unexg  7730  unexOLD  7732  tpex  7733  2oex  8453  en2prd  9032  pw2f1olem  9057  dif1en  9134  opthreg  9575  djuexALT  9896  dfac2b  10102  intwun  10708  wunex2  10711  wuncval2  10720  intgru  10787  xrex  13002  seqexw  14044  pr2pwpr  14506  wwlktovfo  14985  prmreclem2  16967  prdsval  17498  xpsfval  17610  xpssca  17620  xpsvsca  17621  isposix  18370  clatl  18554  ipoval  18576  mgm0b  18705  frmdval  18900  mgmnsgrpex  18983  sgrpnmndex  18984  symg2bas  19454  pmtrprfval  19548  pmtrprfvalrn  19549  psgnprfval1  19583  psgnprfval2  19584  isnzr2hash  20594  psgnghm  21690  psgnco  21693  evpmodpmf1o  21706  mdetralt  22726  m2detleiblem5  22743  m2detleiblem6  22744  m2detleiblem3  22747  m2detleiblem4  22748  m2detleib  22749  indistopon  23119  pptbas  23126  indistpsALT  23131  tuslem  24384  tmslem  24600  ehl2eudis  25542  sqff1o  27304  dchrval  27356  elno  27768  eengv  29238  structvtxvallem  29279  structiedg0val  29281  upgrbi  29352  umgrbi  29360  upgr1e  29372  umgredg  29397  uspgr1e  29503  usgr1e  29504  uspgr1ewop  29507  uspgr2v1e2w  29510  usgr2v1e2w  29511  usgrexmplef  29518  usgrexmpledg  29521  1loopgrnb0  29761  1egrvtxdg1  29768  1egrvtxdg0  29770  umgr2v2evtx  29780  umgr2v2eiedg  29782  umgr2v2e  29784  umgr2v2enb1  29785  umgr2v2evd2  29786  vdegp1ai  29795  vdegp1bi  29796  wlk2v2elem2  30416  wlk2v2e  30417  eupth2lems  30498  frcond2  30527  frcond3  30529  nfrgr2v  30532  frgr3vlem1  30533  frgr3vlem2  30534  frgrncvvdeqlem2  30560  ex-uni  30686  ex-eprel  30693  indf1ofs  33099  idlsrgval  33710  constr0  34044  prsiga  34438  difelsiga  34440  measssd  34522  carsgsigalem  34622  carsgclctun  34628  pmeasmono  34631  eulerpartlemn  34688  probun  34726  coinflipprob  34787  coinflipspace  34788  coinfliprv  34790  coinflippv  34791  cusgredgex  35485  subfacp1lem3  35545  subfacp1lem5  35547  ex-sategoelel12  35790  altopex  36323  altopthsn  36324  altxpsspw  36340  bj-endval  37819  poimirlem9  38140  poimirlem15  38146  tgrpset  41381  hlhilset  42570  aprilfools2025  43268  kelac2lem  43653  kelac2  43654  mendval  43768  tr3dom  44116  fvrcllb0d  44281  fvrcllb0da  44282  fvrcllb1d  44283  corclrcl  44295  corcltrcl  44327  cotrclrcl  44330  clsk1indlem2  44630  clsk1indlem3  44631  clsk1indlem4  44632  clsk1indlem1  44633  mnuprdlem3  44848  mnurndlem1  44855  permaxpr  45584  prsal  46890  sge0pr  46966  elsprel  48079  sprvalpw  48084  prprvalpw  48119  sbcpr  48125  nnsum3primes4  48408  nnsum3primesgbe  48412  opstrgric  48546  stgrfv  48573  stgredgel  48577  usgrexmpl1lem  48641  usgrexmpl1edg  48644  usgrexmpl1tri  48645  usgrexmpl2lem  48646  usgrexmpl2edg  48649  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2nb4  48655  usgrexmpl2nb5  48656  usgrexmpl2trifr  48657  gpgov  48662  gpgvtx  48663  gpgiedg  48664  gpgiedgdmellem  48666  gpgprismgr4cycllem2  48716  gpgprismgr4cycllem3  48717  gpgprismgr4cycllem8  48722  gpgprismgr4cycllem10  48724  pgnbgreunbgr  48745  fprmappr  48976  zlmodzxzlmod  48985  zlmodzxzel  48986  zlmodzxz0  48987  zlmodzxzscm  48988  zlmodzxzadd  48989  zlmodzxzldeplem1  49131  zlmodzxzldeplem3  49133  zlmodzxzldeplem4  49134  ldepsnlinclem1  49136  ldepsnlinclem2  49137  ldepsnlinc  49139  2arymaptfo  49285  prelrrx2  49344  rrx2xpref1o  49349  rrx2plordisom  49354  ehl2eudisval0  49356  rrx2linesl  49374  2sphere0  49381  line2  49383  line2x  49385  line2y  49386  resipos  49604  fucoppcffth  50040  termc2  50147  uobeqterm  50175  incat  50230  onsetreclem1  50334