Theorem prex 5374

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 4706), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.) Avoid ax-nul 5235 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 5373	. . . 4 ⊢ ∃𝑧∀𝑤((𝑤 = 𝐴 ∨ 𝑤 = 𝐵) → 𝑤 ∈ 𝑧)
2	1	sepexi 5230	. . 3 ⊢ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
3		dfcleq 2733	. . . . 5 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}))
4		vex 3436	. . . . . . . 8 ⊢ 𝑤 ∈ V
5	4	elpr 4587	. . . . . . 7 ⊢ (𝑤 ∈ {𝐴, 𝐵} ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵))
6	5	bibi2i 338	. . . . . 6 ⊢ ((𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ (𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
7	6	albii 1826	. . . . 5 ⊢ (∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ {𝐴, 𝐵}) ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
8	3, 7	bitri 276	. . . 4 ⊢ (𝑧 = {𝐴, 𝐵} ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
9	8	exbii 1855	. . 3 ⊢ (∃𝑧 𝑧 = {𝐴, 𝐵} ↔ ∃𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ (𝑤 = 𝐴 ∨ 𝑤 = 𝐵)))
10	2, 9	mpbir 232	. 2 ⊢ ∃𝑧 𝑧 = {𝐴, 𝐵}
11	10	issetri 3451	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:   ↔ wb 207   ∨ wo 853  ∀wal 1545   = wceq 1547  ∃wex 1786   ∈ wcel 2119  Vcvv 3432  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  snex  5375  prelpw  5392  opex  5410  opexOLD  5411  elopg  5413  opi2  5416  op1stb  5418  opth  5423  opeqsng  5451  opeqpr  5453  opthwiener  5462  uniop  5463  opthhausdorff  5465  opthhausdorff0  5466  fr2nr  5602  xpsspw  5759  relop  5799  f1prex  7235  unexg  7693  unexOLD  7695  tpex  7696  2oex  8413  en2prd  8991  pw2f1olem  9016  dif1en  9093  opthreg  9537  djuexALT  9844  dfac2b  10051  intwun  10656  wunex2  10659  wuncval2  10668  intgru  10735  xrex  12935  seqexw  13977  pr2pwpr  14439  wwlktovfo  14918  prmreclem2  16886  prdsval  17416  xpsfval  17528  xpssca  17538  xpsvsca  17539  isposix  18288  clatl  18472  ipoval  18494  mgm0b  18623  frmdval  18817  mgmnsgrpex  18900  sgrpnmndex  18901  symg2bas  19366  pmtrprfval  19460  pmtrprfvalrn  19461  psgnprfval1  19495  psgnprfval2  19496  isnzr2hash  20498  psgnghm  21562  psgnco  21565  evpmodpmf1o  21578  mdetralt  22598  m2detleiblem5  22615  m2detleiblem6  22616  m2detleiblem3  22619  m2detleiblem4  22620  m2detleib  22621  indistopon  22991  pptbas  22998  indistpsALT  23003  tuslem  24256  tmslem  24472  ehl2eudis  25414  sqff1o  27170  dchrval  27222  elno  27634  eengv  29073  structvtxvallem  29114  structiedg0val  29116  upgrbi  29187  umgrbi  29195  upgr1e  29207  umgredg  29232  uspgr1e  29338  usgr1e  29339  uspgr1ewop  29342  uspgr2v1e2w  29345  usgr2v1e2w  29346  usgrexmplef  29353  usgrexmpledg  29356  1loopgrnb0  29596  1egrvtxdg1  29603  1egrvtxdg0  29605  umgr2v2evtx  29615  umgr2v2eiedg  29617  umgr2v2e  29619  umgr2v2enb1  29620  umgr2v2evd2  29621  vdegp1ai  29630  vdegp1bi  29631  wlk2v2elem2  30251  wlk2v2e  30252  eupth2lems  30333  frcond2  30362  frcond3  30364  nfrgr2v  30367  frgr3vlem1  30368  frgr3vlem2  30369  frgrncvvdeqlem2  30395  ex-uni  30521  ex-eprel  30528  indf1ofs  32952  idlsrgval  33593  constr0  33928  prsiga  34322  difelsiga  34324  measssd  34406  carsgsigalem  34506  carsgclctun  34512  pmeasmono  34515  eulerpartlemn  34572  probun  34610  coinflipprob  34671  coinflipspace  34672  coinfliprv  34674  coinflippv  34675  cusgredgex  35357  subfacp1lem3  35417  subfacp1lem5  35419  ex-sategoelel12  35662  altopex  36195  altopthsn  36196  altxpsspw  36212  bj-endval  37682  poimirlem9  38003  poimirlem15  38009  tgrpset  41244  hlhilset  42433  aprilfools2025  43131  kelac2lem  43516  kelac2  43517  mendval  43631  tr3dom  43979  fvrcllb0d  44144  fvrcllb0da  44145  fvrcllb1d  44146  corclrcl  44158  corcltrcl  44190  cotrclrcl  44193  clsk1indlem2  44493  clsk1indlem3  44494  clsk1indlem4  44495  clsk1indlem1  44496  mnuprdlem3  44725  mnurndlem1  44732  permaxpr  45461  prsal  46768  sge0pr  46844  elsprel  47957  sprvalpw  47962  prprvalpw  47997  sbcpr  48003  nnsum3primes4  48286  nnsum3primesgbe  48290  opstrgric  48424  stgrfv  48451  stgredgel  48455  usgrexmpl1lem  48519  usgrexmpl1edg  48522  usgrexmpl1tri  48523  usgrexmpl2lem  48524  usgrexmpl2edg  48527  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2nb4  48533  usgrexmpl2nb5  48534  usgrexmpl2trifr  48535  gpgov  48540  gpgvtx  48541  gpgiedg  48542  gpgiedgdmellem  48544  gpgprismgr4cycllem2  48594  gpgprismgr4cycllem3  48595  gpgprismgr4cycllem8  48600  gpgprismgr4cycllem10  48602  pgnbgreunbgr  48623  fprmappr  48843  zlmodzxzlmod  48852  zlmodzxzel  48853  zlmodzxz0  48854  zlmodzxzscm  48855  zlmodzxzadd  48856  zlmodzxzldeplem1  48998  zlmodzxzldeplem3  49000  zlmodzxzldeplem4  49001  ldepsnlinclem1  49003  ldepsnlinclem2  49004  ldepsnlinc  49006  2arymaptfo  49152  prelrrx2  49211  rrx2xpref1o  49216  rrx2plordisom  49221  ehl2eudisval0  49223  rrx2linesl  49241  2sphere0  49248  line2  49250  line2x  49252  line2y  49253  resipos  49472  fucoppcffth  49908  termc2  50015  uobeqterm  50043  incat  50098  onsetreclem1  50202