Theorem prex 5380

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 4711), 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 5379	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5236	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2729	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3433	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4592	. . . . . . 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 3448	1 ⊢ {𝐴, 𝐵} ∈ V

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

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  snex  5381  prelpw  5398  opex  5416  opexOLD  5417  elopg  5419  opi2  5422  op1stb  5424  opth  5429  opeqsng  5457  opeqpr  5459  opthwiener  5468  uniop  5469  opthhausdorff  5471  opthhausdorff0  5472  fr2nr  5608  xpsspw  5765  relop  5805  f1prex  7239  unexg  7697  unexOLD  7699  tpex  7700  2oex  8416  en2prd  8994  pw2f1olem  9019  dif1en  9096  opthreg  9539  djuexALT  9846  dfac2b  10053  intwun  10658  wunex2  10661  wuncval2  10670  intgru  10737  xrex  12937  seqexw  13979  pr2pwpr  14441  wwlktovfo  14920  prmreclem2  16888  prdsval  17418  xpsfval  17530  xpssca  17540  xpsvsca  17541  isposix  18290  clatl  18474  ipoval  18496  mgm0b  18625  frmdval  18819  mgmnsgrpex  18902  sgrpnmndex  18903  symg2bas  19368  pmtrprfval  19462  pmtrprfvalrn  19463  psgnprfval1  19497  psgnprfval2  19498  isnzr2hash  20496  psgnghm  21560  psgnco  21563  evpmodpmf1o  21576  mdetralt  22573  m2detleiblem5  22590  m2detleiblem6  22591  m2detleiblem3  22594  m2detleiblem4  22595  m2detleib  22596  indistopon  22966  pptbas  22973  indistpsALT  22978  tuslem  24231  tmslem  24447  ehl2eudis  25389  sqff1o  27145  dchrval  27197  elno  27609  eengv  29048  structvtxvallem  29089  structiedg0val  29091  upgrbi  29162  umgrbi  29170  upgr1e  29182  umgredg  29207  uspgr1e  29313  usgr1e  29314  uspgr1ewop  29317  uspgr2v1e2w  29320  usgr2v1e2w  29321  usgrexmplef  29328  usgrexmpledg  29331  1loopgrnb0  29571  1egrvtxdg1  29578  1egrvtxdg0  29580  umgr2v2evtx  29590  umgr2v2eiedg  29592  umgr2v2e  29594  umgr2v2enb1  29595  umgr2v2evd2  29596  vdegp1ai  29605  vdegp1bi  29606  wlk2v2elem2  30226  wlk2v2e  30227  eupth2lems  30308  frcond2  30337  frcond3  30339  nfrgr2v  30342  frgr3vlem1  30343  frgr3vlem2  30344  frgrncvvdeqlem2  30370  ex-uni  30496  ex-eprel  30503  indf1ofs  32926  idlsrgval  33563  constr0  33881  prsiga  34275  difelsiga  34277  measssd  34359  carsgsigalem  34459  carsgclctun  34465  pmeasmono  34468  eulerpartlemn  34525  probun  34563  coinflipprob  34624  coinflipspace  34625  coinfliprv  34627  coinflippv  34628  cusgredgex  35304  subfacp1lem3  35364  subfacp1lem5  35366  ex-sategoelel12  35609  altopex  36142  altopthsn  36143  altxpsspw  36159  bj-endval  37629  poimirlem9  37950  poimirlem15  37956  tgrpset  41191  hlhilset  42380  aprilfools2025  43107  kelac2lem  43492  kelac2  43493  mendval  43607  tr3dom  43955  fvrcllb0d  44120  fvrcllb0da  44121  fvrcllb1d  44122  corclrcl  44134  corcltrcl  44166  cotrclrcl  44169  clsk1indlem2  44469  clsk1indlem3  44470  clsk1indlem4  44471  clsk1indlem1  44472  mnuprdlem3  44701  mnurndlem1  44708  permaxpr  45437  prsal  46746  sge0pr  46822  elsprel  47935  sprvalpw  47940  prprvalpw  47975  sbcpr  47981  nnsum3primes4  48264  nnsum3primesgbe  48268  opstrgric  48402  stgrfv  48429  stgredgel  48433  usgrexmpl1lem  48497  usgrexmpl1edg  48500  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2edg  48505  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2nb4  48511  usgrexmpl2nb5  48512  usgrexmpl2trifr  48513  gpgov  48518  gpgvtx  48519  gpgiedg  48520  gpgiedgdmellem  48522  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem3  48573  gpgprismgr4cycllem8  48578  gpgprismgr4cycllem10  48580  pgnbgreunbgr  48601  fprmappr  48821  zlmodzxzlmod  48830  zlmodzxzel  48831  zlmodzxz0  48832  zlmodzxzscm  48833  zlmodzxzadd  48834  zlmodzxzldeplem1  48976  zlmodzxzldeplem3  48978  zlmodzxzldeplem4  48979  ldepsnlinclem1  48981  ldepsnlinclem2  48982  ldepsnlinc  48984  2arymaptfo  49130  prelrrx2  49189  rrx2xpref1o  49194  rrx2plordisom  49199  ehl2eudisval0  49201  rrx2linesl  49219  2sphere0  49226  line2  49228  line2x  49230  line2y  49231  resipos  49450  fucoppcffth  49886  termc2  49993  uobeqterm  50021  incat  50076  onsetreclem1  50180