Theorem prex 5375

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 4712), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5241 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 5374	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5236	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2730	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3434	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4593	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 337	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1821	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 275	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1850	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 231	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3449	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:   ↔ wb 206   ∨ wo 848  ∀wal 1540   = wceq 1542  ∃wex 1781   ∈ wcel 2114  Vcvv 3430  {cpr 4570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  snex  5376  prelpw  5393  opex  5411  opexOLD  5412  elopg  5414  opi2  5417  op1stb  5419  opth  5424  opeqsng  5451  opeqpr  5453  opthwiener  5462  uniop  5463  opthhausdorff  5465  opthhausdorff0  5466  fr2nr  5601  xpsspw  5758  relop  5799  f1prex  7232  unexg  7690  unexOLD  7692  tpex  7693  2oex  8409  en2prd  8987  pw2f1olem  9012  dif1en  9089  opthreg  9530  djuexALT  9837  dfac2b  10044  intwun  10649  wunex2  10652  wuncval2  10661  intgru  10728  xrex  12928  seqexw  13970  pr2pwpr  14432  wwlktovfo  14911  prmreclem2  16879  prdsval  17409  xpsfval  17521  xpssca  17531  xpsvsca  17532  isposix  18281  clatl  18465  ipoval  18487  mgm0b  18616  frmdval  18810  mgmnsgrpex  18893  sgrpnmndex  18894  symg2bas  19359  pmtrprfval  19453  pmtrprfvalrn  19454  psgnprfval1  19488  psgnprfval2  19489  isnzr2hash  20487  psgnghm  21570  psgnco  21573  evpmodpmf1o  21586  mdetralt  22583  m2detleiblem5  22600  m2detleiblem6  22601  m2detleiblem3  22604  m2detleiblem4  22605  m2detleib  22606  indistopon  22976  pptbas  22983  indistpsALT  22988  tuslem  24241  tmslem  24457  ehl2eudis  25399  sqff1o  27159  dchrval  27211  elno  27623  eengv  29062  structvtxvallem  29103  structiedg0val  29105  upgrbi  29176  umgrbi  29184  upgr1e  29196  umgredg  29221  uspgr1e  29327  usgr1e  29328  uspgr1ewop  29331  uspgr2v1e2w  29334  usgr2v1e2w  29335  usgrexmplef  29342  usgrexmpledg  29345  1loopgrnb0  29586  1egrvtxdg1  29593  1egrvtxdg0  29595  umgr2v2evtx  29605  umgr2v2eiedg  29607  umgr2v2e  29609  umgr2v2enb1  29610  umgr2v2evd2  29611  vdegp1ai  29620  vdegp1bi  29621  wlk2v2elem2  30241  wlk2v2e  30242  eupth2lems  30323  frcond2  30352  frcond3  30354  nfrgr2v  30357  frgr3vlem1  30358  frgr3vlem2  30359  frgrncvvdeqlem2  30385  ex-uni  30511  ex-eprel  30518  indf1ofs  32941  idlsrgval  33578  constr0  33897  prsiga  34291  difelsiga  34293  measssd  34375  carsgsigalem  34475  carsgclctun  34481  pmeasmono  34484  eulerpartlemn  34541  probun  34579  coinflipprob  34640  coinflipspace  34641  coinfliprv  34643  coinflippv  34644  cusgredgex  35320  subfacp1lem3  35380  subfacp1lem5  35382  ex-sategoelel12  35625  altopex  36158  altopthsn  36159  altxpsspw  36175  bj-endval  37645  poimirlem9  37964  poimirlem15  37970  tgrpset  41205  hlhilset  42394  aprilfools2025  43121  kelac2lem  43510  kelac2  43511  mendval  43625  tr3dom  43973  fvrcllb0d  44138  fvrcllb0da  44139  fvrcllb1d  44140  corclrcl  44152  corcltrcl  44184  cotrclrcl  44187  clsk1indlem2  44487  clsk1indlem3  44488  clsk1indlem4  44489  clsk1indlem1  44490  mnuprdlem3  44719  mnurndlem1  44726  permaxpr  45455  prsal  46764  sge0pr  46840  elsprel  47947  sprvalpw  47952  prprvalpw  47987  sbcpr  47993  nnsum3primes4  48276  nnsum3primesgbe  48280  opstrgric  48414  stgrfv  48441  stgredgel  48445  usgrexmpl1lem  48509  usgrexmpl1edg  48512  usgrexmpl1tri  48513  usgrexmpl2lem  48514  usgrexmpl2edg  48517  usgrexmpl2nb0  48519  usgrexmpl2nb1  48520  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2nb4  48523  usgrexmpl2nb5  48524  usgrexmpl2trifr  48525  gpgov  48530  gpgvtx  48531  gpgiedg  48532  gpgiedgdmellem  48534  gpgprismgr4cycllem2  48584  gpgprismgr4cycllem3  48585  gpgprismgr4cycllem8  48590  gpgprismgr4cycllem10  48592  pgnbgreunbgr  48613  fprmappr  48833  zlmodzxzlmod  48842  zlmodzxzel  48843  zlmodzxz0  48844  zlmodzxzscm  48845  zlmodzxzadd  48846  zlmodzxzldeplem1  48988  zlmodzxzldeplem3  48990  zlmodzxzldeplem4  48991  ldepsnlinclem1  48993  ldepsnlinclem2  48994  ldepsnlinc  48996  2arymaptfo  49142  prelrrx2  49201  rrx2xpref1o  49206  rrx2plordisom  49211  ehl2eudisval0  49213  rrx2linesl  49231  2sphere0  49238  line2  49240  line2x  49242  line2y  49243  resipos  49462  fucoppcffth  49898  termc2  50005  uobeqterm  50033  incat  50088  onsetreclem1  50192