Theorem prex 5384

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 4726), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5253 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 5383	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5248	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2730	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3446	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4607	. . . . . . 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 3461	1 ⊢ {𝐴, 𝐵} ∈ V

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

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 5243  ax-pr 5379

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 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  snex  5385  prelpw  5401  opex  5419  opexOLD  5420  elopg  5422  opi2  5425  op1stb  5427  opth  5432  opeqsng  5459  opeqpr  5461  opthwiener  5470  uniop  5471  opthhausdorff  5473  opthhausdorff0  5474  fr2nr  5609  xpsspw  5766  relop  5807  f1prex  7240  unexg  7698  unexOLD  7700  tpex  7701  2oex  8418  en2prd  8996  pw2f1olem  9021  dif1en  9098  opthreg  9539  djuexALT  9846  dfac2b  10053  intwun  10658  wunex2  10661  wuncval2  10670  intgru  10737  xrex  12912  seqexw  13952  pr2pwpr  14414  wwlktovfo  14893  prmreclem2  16857  prdsval  17387  xpsfval  17499  xpssca  17509  xpsvsca  17510  isposix  18259  clatl  18443  ipoval  18465  mgm0b  18594  frmdval  18788  mgmnsgrpex  18868  sgrpnmndex  18869  symg2bas  19334  pmtrprfval  19428  pmtrprfvalrn  19429  psgnprfval1  19463  psgnprfval2  19464  isnzr2hash  20464  psgnghm  21547  psgnco  21550  evpmodpmf1o  21563  mdetralt  22564  m2detleiblem5  22581  m2detleiblem6  22582  m2detleiblem3  22585  m2detleiblem4  22586  m2detleib  22587  indistopon  22957  pptbas  22964  indistpsALT  22969  tuslem  24222  tmslem  24438  ehl2eudis  25390  sqff1o  27160  dchrval  27213  elno  27625  eengv  29064  structvtxvallem  29105  structiedg0val  29107  upgrbi  29178  umgrbi  29186  upgr1e  29198  umgredg  29223  uspgr1e  29329  usgr1e  29330  uspgr1ewop  29333  uspgr2v1e2w  29336  usgr2v1e2w  29337  usgrexmplef  29344  usgrexmpledg  29347  1loopgrnb0  29588  1egrvtxdg1  29595  1egrvtxdg0  29597  umgr2v2evtx  29607  umgr2v2eiedg  29609  umgr2v2e  29611  umgr2v2enb1  29612  umgr2v2evd2  29613  vdegp1ai  29622  vdegp1bi  29623  wlk2v2elem2  30243  wlk2v2e  30244  eupth2lems  30325  frcond2  30354  frcond3  30356  nfrgr2v  30359  frgr3vlem1  30360  frgr3vlem2  30361  frgrncvvdeqlem2  30387  ex-uni  30513  ex-eprel  30520  indf1ofs  32958  idlsrgval  33595  constr0  33914  prsiga  34308  difelsiga  34310  measssd  34392  carsgsigalem  34492  carsgclctun  34498  pmeasmono  34501  eulerpartlemn  34558  probun  34596  coinflipprob  34657  coinflipspace  34658  coinfliprv  34660  coinflippv  34661  cusgredgex  35335  subfacp1lem3  35395  subfacp1lem5  35397  ex-sategoelel12  35640  altopex  36173  altopthsn  36174  altxpsspw  36190  bj-endval  37564  poimirlem9  37874  poimirlem15  37880  tgrpset  41115  hlhilset  42304  aprilfools2025  43026  kelac2lem  43415  kelac2  43416  mendval  43530  tr3dom  43878  fvrcllb0d  44043  fvrcllb0da  44044  fvrcllb1d  44045  corclrcl  44057  corcltrcl  44089  cotrclrcl  44092  clsk1indlem2  44392  clsk1indlem3  44393  clsk1indlem4  44394  clsk1indlem1  44395  mnuprdlem3  44624  mnurndlem1  44631  permaxpr  45360  prsal  46670  sge0pr  46746  elsprel  47829  sprvalpw  47834  prprvalpw  47869  sbcpr  47875  nnsum3primes4  48142  nnsum3primesgbe  48146  opstrgric  48280  stgrfv  48307  stgredgel  48311  usgrexmpl1lem  48375  usgrexmpl1edg  48378  usgrexmpl1tri  48379  usgrexmpl2lem  48380  usgrexmpl2edg  48383  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2nb4  48389  usgrexmpl2nb5  48390  usgrexmpl2trifr  48391  gpgov  48396  gpgvtx  48397  gpgiedg  48398  gpgiedgdmellem  48400  gpgprismgr4cycllem2  48450  gpgprismgr4cycllem3  48451  gpgprismgr4cycllem8  48456  gpgprismgr4cycllem10  48458  pgnbgreunbgr  48479  fprmappr  48699  zlmodzxzlmod  48708  zlmodzxzel  48709  zlmodzxz0  48710  zlmodzxzscm  48711  zlmodzxzadd  48712  zlmodzxzldeplem1  48854  zlmodzxzldeplem3  48856  zlmodzxzldeplem4  48857  ldepsnlinclem1  48859  ldepsnlinclem2  48860  ldepsnlinc  48862  2arymaptfo  49008  prelrrx2  49067  rrx2xpref1o  49072  rrx2plordisom  49077  ehl2eudisval0  49079  rrx2linesl  49097  2sphere0  49104  line2  49106  line2x  49108  line2y  49109  resipos  49328  fucoppcffth  49764  termc2  49871  uobeqterm  49899  incat  49954  onsetreclem1  50058