Theorem prex 5395

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 4724), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5259 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 5394	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5255	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2753	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3454	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4605	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 340	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1851	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 278	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1880	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 234	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3469	1 ⊢ {𝐴, 𝐵} ∈ V

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144  Vcvv 3450  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  snex  5396  prelpw  5413  opex  5431  opexOLD  5432  elopg  5434  opi2  5437  op1stb  5439  opth  5444  opeqsng  5474  opeqpr  5476  opthwiener  5486  uniop  5487  opthhausdorff  5489  opthhausdorff0  5490  fr2nr  5627  xpsspw  5786  relop  5827  f1prex  7292  unexg  7760  tpex  7762  2oex  8491  en2prd  9078  pw2f1olem  9103  dif1en  9180  opthreg  9622  djuexALT  10006  dfac2b  10212  intwun  10823  wunex2  10826  wuncval2  10835  intgru  10902  xrex  13118  seqexw  14163  pr2pwpr  14627  wwlktovfo  15116  prmreclem2  17100  prdsval  17631  xpsfval  17743  xpssca  17753  xpsvsca  17754  isposix  18503  clatl  18687  ipoval  18709  mgm0b  18840  frmdval  19052  mgmnsgrpex  19135  sgrpnmndex  19136  degenmgmbas  19140  degenmgm2  19145  symg2bas  19612  pmtrprfval  19706  pmtrprfvalrn  19707  psgnprfval1  19741  psgnprfval2  19742  isnzr2hash  20775  psgnghm  21891  psgnco  21894  evpmodpmf1o  21907  mdetralt  22928  m2detleiblem5  22945  m2detleiblem6  22946  m2detleiblem3  22949  m2detleiblem4  22950  m2detleib  22951  indistopon  23324  pptbas  23331  indistpsALT  23336  tuslem  24590  tmslem  24806  ehl2eudis  25748  sqff1o  27514  dchrval  27566  elno  28008  eengv  29562  structvtxvallem  29603  structiedg0val  29605  upgrbi  29676  umgrbi  29684  upgr1e  29696  umgredg  29721  uspgr1e  29830  usgr1e  29831  uspgr1ewop  29834  uspgr2v1e2w  29837  usgr2v1e2w  29838  usgrexmplef  29845  usgrexmpledg  29848  1loopgrnb0  30088  1egrvtxdg1  30095  1egrvtxdg0  30097  umgr2v2evtx  30107  umgr2v2eiedg  30109  umgr2v2e  30111  umgr2v2enb1  30112  umgr2v2evd2  30113  vdegp1ai  30122  vdegp1bi  30123  wlk2v2elem2  30762  wlk2v2e  30763  eupth2lems  30844  frcond2  30873  frcond3  30875  nfrgr2v  30878  frgr3vlem1  30879  frgr3vlem2  30880  frgrncvvdeqlem2  30906  ex-uni  31032  ex-eprel  31039  indf1ofs  33479  idlsrgval  34081  constr0  34415  prsiga  34809  measssd  34894  carsgsigalem  34993  carsgclctun  34999  pmeasmono  35002  eulerpartlemn  35059  probun  35097  coinflipprob  35158  coinflipspace  35159  coinfliprv  35161  coinflippv  35162  cusgredgex  35982  subfacp1lem3  36033  subfacp1lem5  36035  ex-sategoelel12  36278  altopex  36817  altopthsn  36818  altxpsspw  36834  bj-endval  38329  poimirlem9  38640  poimirlem15  38646  impprop  38737  tgrpset  41895  hlhilset  43084  aprilfools2025  43778  kelac2lem  44159  kelac2  44160  mendval  44274  tr3dom  44622  fvrcllb0d  44786  fvrcllb0da  44787  fvrcllb1d  44788  corclrcl  44800  corcltrcl  44832  cotrclrcl  44835  clsk1indlem2  45135  clsk1indlem3  45136  clsk1indlem4  45137  clsk1indlem1  45138  mnuprdlem3  45351  mnurndlem1  45358  permaxpr  46093  prsal  47421  sge0pr  47497  elsprel  48650  sprvalpw  48655  prprvalpw  48690  sbcpr  48696  nnsum3primes4  48979  nnsum3primesgbe  48983  opstrgric  49117  stgrfv  49144  stgredgel  49148  usgrexmpl1lem  49212  usgrexmpl1edg  49215  usgrexmpl1tri  49216  usgrexmpl2lem  49217  usgrexmpl2edg  49220  usgrexmpl2nb0  49222  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2nb4  49226  usgrexmpl2nb5  49227  usgrexmpl2trifr  49228  gpgov  49233  gpgvtx  49234  gpgiedg  49235  gpgiedgdmellem  49237  gpgprismgr4cycllem2  49287  gpgprismgr4cycllem3  49288  gpgprismgr4cycllem8  49293  gpgprismgr4cycllem10  49295  pgnbgreunbgr  49316  fprmappr  49550  zlmodzxzlmod  49559  zlmodzxzel  49560  zlmodzxz0  49561  zlmodzxzscm  49562  zlmodzxzadd  49563  zlmodzxzldeplem1  49705  zlmodzxzldeplem3  49707  zlmodzxzldeplem4  49708  ldepsnlinclem1  49710  ldepsnlinclem2  49711  ldepsnlinc  49713  2arymaptfo  49859  resipos  50182  fucoppcffth  50639  termc2  50746  uobeqterm  50777  incat  50832  onsetreclem1  50966