Theorem prex 5394

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 4725), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5255 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 5393	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5250	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2754	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3457	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4606	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 339	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1838	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 277	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1867	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 233	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3472	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:   ↔ wb 208   ∨ wo 858  ∀wal 1557   = wceq 1559  ∃wex 1798   ∈ wcel 2141  Vcvv 3453  {cpr 4583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4582  df-pr 4584

This theorem is referenced by:  snex  5395  prelpw  5412  opex  5430  opexOLD  5431  elopg  5433  opi2  5436  op1stb  5438  opth  5443  opeqsng  5471  opeqpr  5473  opthwiener  5482  uniop  5483  opthhausdorff  5485  opthhausdorff0  5486  fr2nr  5622  xpsspw  5780  relop  5820  f1prex  7264  unexg  7722  unexOLD  7724  tpex  7725  2oex  8444  en2prd  9024  pw2f1olem  9049  dif1en  9126  opthreg  9570  djuexALT  9877  dfac2b  10084  intwun  10690  wunex2  10693  wuncval2  10702  intgru  10769  xrex  12985  seqexw  14027  pr2pwpr  14489  wwlktovfo  14968  prmreclem2  16936  prdsval  17467  xpsfval  17579  xpssca  17589  xpsvsca  17590  isposix  18339  clatl  18523  ipoval  18545  mgm0b  18674  frmdval  18868  mgmnsgrpex  18951  sgrpnmndex  18952  symg2bas  19416  pmtrprfval  19510  pmtrprfvalrn  19511  psgnprfval1  19545  psgnprfval2  19546  isnzr2hash  20548  psgnghm  21612  psgnco  21615  evpmodpmf1o  21628  mdetralt  22648  m2detleiblem5  22665  m2detleiblem6  22666  m2detleiblem3  22669  m2detleiblem4  22670  m2detleib  22671  indistopon  23041  pptbas  23048  indistpsALT  23053  tuslem  24306  tmslem  24522  ehl2eudis  25464  sqff1o  27223  dchrval  27275  elno  27687  eengv  29126  structvtxvallem  29167  structiedg0val  29169  upgrbi  29240  umgrbi  29248  upgr1e  29260  umgredg  29285  uspgr1e  29391  usgr1e  29392  uspgr1ewop  29395  uspgr2v1e2w  29398  usgr2v1e2w  29399  usgrexmplef  29406  usgrexmpledg  29409  1loopgrnb0  29649  1egrvtxdg1  29656  1egrvtxdg0  29658  umgr2v2evtx  29668  umgr2v2eiedg  29670  umgr2v2e  29672  umgr2v2enb1  29673  umgr2v2evd2  29674  vdegp1ai  29683  vdegp1bi  29684  wlk2v2elem2  30304  wlk2v2e  30305  eupth2lems  30386  frcond2  30415  frcond3  30417  nfrgr2v  30420  frgr3vlem1  30421  frgr3vlem2  30422  frgrncvvdeqlem2  30448  ex-uni  30574  ex-eprel  30581  indf1ofs  33005  idlsrgval  33660  constr0  33995  prsiga  34389  difelsiga  34391  measssd  34473  carsgsigalem  34573  carsgclctun  34579  pmeasmono  34582  eulerpartlemn  34639  probun  34677  coinflipprob  34738  coinflipspace  34739  coinfliprv  34741  coinflippv  34742  cusgredgex  35436  subfacp1lem3  35496  subfacp1lem5  35498  ex-sategoelel12  35741  altopex  36274  altopthsn  36275  altxpsspw  36291  bj-endval  37771  poimirlem9  38092  poimirlem15  38098  tgrpset  41333  hlhilset  42522  aprilfools2025  43220  kelac2lem  43605  kelac2  43606  mendval  43720  tr3dom  44068  fvrcllb0d  44233  fvrcllb0da  44234  fvrcllb1d  44235  corclrcl  44247  corcltrcl  44279  cotrclrcl  44282  clsk1indlem2  44582  clsk1indlem3  44583  clsk1indlem4  44584  clsk1indlem1  44585  mnuprdlem3  44814  mnurndlem1  44821  permaxpr  45550  prsal  46856  sge0pr  46932  elsprel  48045  sprvalpw  48050  prprvalpw  48085  sbcpr  48091  nnsum3primes4  48374  nnsum3primesgbe  48378  opstrgric  48512  stgrfv  48539  stgredgel  48543  usgrexmpl1lem  48607  usgrexmpl1edg  48610  usgrexmpl1tri  48611  usgrexmpl2lem  48612  usgrexmpl2edg  48615  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2nb4  48621  usgrexmpl2nb5  48622  usgrexmpl2trifr  48623  gpgov  48628  gpgvtx  48629  gpgiedg  48630  gpgiedgdmellem  48632  gpgprismgr4cycllem2  48682  gpgprismgr4cycllem3  48683  gpgprismgr4cycllem8  48688  gpgprismgr4cycllem10  48690  pgnbgreunbgr  48711  fprmappr  48931  zlmodzxzlmod  48940  zlmodzxzel  48941  zlmodzxz0  48942  zlmodzxzscm  48943  zlmodzxzadd  48944  zlmodzxzldeplem1  49086  zlmodzxzldeplem3  49088  zlmodzxzldeplem4  49089  ldepsnlinclem1  49091  ldepsnlinclem2  49092  ldepsnlinc  49094  2arymaptfo  49240  prelrrx2  49299  rrx2xpref1o  49304  rrx2plordisom  49309  ehl2eudisval0  49311  rrx2linesl  49329  2sphere0  49336  line2  49338  line2x  49340  line2y  49341  resipos  49560  fucoppcffth  49996  termc2  50103  uobeqterm  50131  incat  50186  onsetreclem1  50290