Theorem prex 5411

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 4734), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5270 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 5410	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5265	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2756	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3459	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4615	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 340	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1849	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 278	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1878	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 234	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3474	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:   ↔ wb 209   ∨ wo 860  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143  Vcvv 3455  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  snex  5412  prelpw  5429  opex  5447  opexOLD  5448  elopg  5450  opi2  5453  op1stb  5455  opth  5460  opeqsng  5488  opeqpr  5490  opthwiener  5499  uniop  5500  opthhausdorff  5502  opthhausdorff0  5503  fr2nr  5640  xpsspw  5798  relop  5838  f1prex  7284  unexg  7743  unexOLD  7745  tpex  7746  2oex  8466  en2prd  9045  pw2f1olem  9070  dif1en  9147  opthreg  9588  djuexALT  9909  dfac2b  10115  intwun  10721  wunex2  10724  wuncval2  10733  intgru  10800  xrex  13012  seqexw  14055  pr2pwpr  14518  wwlktovfo  14997  prmreclem2  16978  prdsval  17509  xpsfval  17621  xpssca  17631  xpsvsca  17632  isposix  18381  clatl  18565  ipoval  18587  mgm0b  18716  frmdval  18911  mgmnsgrpex  18994  sgrpnmndex  18995  symg2bas  19464  pmtrprfval  19558  pmtrprfvalrn  19559  psgnprfval1  19593  psgnprfval2  19594  isnzr2hash  20604  psgnghm  21711  psgnco  21714  evpmodpmf1o  21727  mdetralt  22746  m2detleiblem5  22763  m2detleiblem6  22764  m2detleiblem3  22767  m2detleiblem4  22768  m2detleib  22769  indistopon  23139  pptbas  23146  indistpsALT  23151  tuslem  24404  tmslem  24620  ehl2eudis  25562  sqff1o  27327  dchrval  27379  elno  27791  eengv  29310  structvtxvallem  29351  structiedg0val  29353  upgrbi  29424  umgrbi  29432  upgr1e  29444  umgredg  29469  uspgr1e  29575  usgr1e  29576  uspgr1ewop  29579  uspgr2v1e2w  29582  usgr2v1e2w  29583  usgrexmplef  29590  usgrexmpledg  29593  1loopgrnb0  29833  1egrvtxdg1  29840  1egrvtxdg0  29842  umgr2v2evtx  29852  umgr2v2eiedg  29854  umgr2v2e  29856  umgr2v2enb1  29857  umgr2v2evd2  29858  vdegp1ai  29867  vdegp1bi  29868  wlk2v2elem2  30488  wlk2v2e  30489  eupth2lems  30570  frcond2  30599  frcond3  30601  nfrgr2v  30604  frgr3vlem1  30605  frgr3vlem2  30606  frgrncvvdeqlem2  30632  ex-uni  30758  ex-eprel  30765  indf1ofs  33167  idlsrgval  33774  constr0  34108  prsiga  34502  difelsiga  34504  measssd  34586  carsgsigalem  34686  carsgclctun  34692  pmeasmono  34695  eulerpartlemn  34752  probun  34790  coinflipprob  34851  coinflipspace  34852  coinfliprv  34854  coinflippv  34855  cusgredgex  35595  subfacp1lem3  35655  subfacp1lem5  35657  ex-sategoelel12  35900  altopex  36433  altopthsn  36434  altxpsspw  36450  bj-endval  37940  poimirlem9  38261  poimirlem15  38267  tgrpset  41500  hlhilset  42689  aprilfools2025  43389  kelac2lem  43774  kelac2  43775  mendval  43889  tr3dom  44237  fvrcllb0d  44402  fvrcllb0da  44403  fvrcllb1d  44404  corclrcl  44416  corcltrcl  44448  cotrclrcl  44451  clsk1indlem2  44751  clsk1indlem3  44752  clsk1indlem4  44753  clsk1indlem1  44754  mnuprdlem3  44967  mnurndlem1  44974  permaxpr  45702  prsal  47015  sge0pr  47091  elsprel  48207  sprvalpw  48212  prprvalpw  48247  sbcpr  48253  nnsum3primes4  48536  nnsum3primesgbe  48540  opstrgric  48674  stgrfv  48701  stgredgel  48705  usgrexmpl1lem  48769  usgrexmpl1edg  48772  usgrexmpl1tri  48773  usgrexmpl2lem  48774  usgrexmpl2edg  48777  usgrexmpl2nb0  48779  usgrexmpl2nb1  48780  usgrexmpl2nb2  48781  usgrexmpl2nb3  48782  usgrexmpl2nb4  48783  usgrexmpl2nb5  48784  usgrexmpl2trifr  48785  gpgov  48790  gpgvtx  48791  gpgiedg  48792  gpgiedgdmellem  48794  gpgprismgr4cycllem2  48844  gpgprismgr4cycllem3  48845  gpgprismgr4cycllem8  48850  gpgprismgr4cycllem10  48852  pgnbgreunbgr  48873  fprmappr  49108  zlmodzxzlmod  49117  zlmodzxzel  49118  zlmodzxz0  49119  zlmodzxzscm  49120  zlmodzxzadd  49121  zlmodzxzldeplem1  49263  zlmodzxzldeplem3  49265  zlmodzxzldeplem4  49266  ldepsnlinclem1  49268  ldepsnlinclem2  49269  ldepsnlinc  49271  2arymaptfo  49417  prelrrx2  49476  rrx2xpref1o  49481  rrx2plordisom  49486  ehl2eudisval0  49488  rrx2linesl  49506  2sphere0  49513  line2  49515  line2x  49517  line2y  49518  resipos  49736  fucoppcffth  50172  termc2  50279  uobeqterm  50307  incat  50362  onsetreclem1  50466