Theorem prex 5377

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 4719), so we can dispense with hypotheses requiring them to be sets. (Contributed by NM, 15-Jul-1993.)

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		preq2 4686	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2818	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5373	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3508	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4685	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2818	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3507	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4717	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5376	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2841	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4718	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5376	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2841	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ∈ wcel 2113  Vcvv 3437  {csn 4575  {cpr 4577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-un 3903  df-nul 4283  df-sn 4576  df-pr 4578

This theorem is referenced by:  prelpw  5389  opex  5407  elopg  5409  opi2  5412  op1stb  5414  opth  5419  opeqsng  5446  opeqpr  5448  opthwiener  5457  uniop  5458  opthhausdorff  5460  opthhausdorff0  5461  fr2nr  5596  xpsspw  5753  relop  5794  f1prex  7224  unexg  7682  unexOLD  7684  tpex  7685  2oex  8402  en2prd  8976  pw2f1olem  9001  dif1en  9078  opthreg  9515  djuexALT  9822  dfac2b  10029  intwun  10633  wunex2  10636  wuncval2  10645  intgru  10712  xrex  12887  seqexw  13926  pr2pwpr  14388  wwlktovfo  14867  prmreclem2  16831  prdsval  17361  xpsfval  17472  xpssca  17482  xpsvsca  17483  isposix  18232  clatl  18416  ipoval  18438  mgm0b  18567  frmdval  18761  mgmnsgrpex  18841  sgrpnmndex  18842  symg2bas  19307  pmtrprfval  19401  pmtrprfvalrn  19402  psgnprfval1  19436  psgnprfval2  19437  isnzr2hash  20436  psgnghm  21519  psgnco  21522  evpmodpmf1o  21535  mdetralt  22524  m2detleiblem5  22541  m2detleiblem6  22542  m2detleiblem3  22545  m2detleiblem4  22546  m2detleib  22547  indistopon  22917  pptbas  22924  indistpsALT  22929  tuslem  24182  tmslem  24398  ehl2eudis  25350  sqff1o  27120  dchrval  27173  elno  27585  eengv  28959  structvtxvallem  29000  structiedg0val  29002  upgrbi  29073  umgrbi  29081  upgr1e  29093  umgredg  29118  uspgr1e  29224  usgr1e  29225  uspgr1ewop  29228  uspgr2v1e2w  29231  usgr2v1e2w  29232  usgrexmplef  29239  usgrexmpledg  29242  1loopgrnb0  29483  1egrvtxdg1  29490  1egrvtxdg0  29492  umgr2v2evtx  29502  umgr2v2eiedg  29504  umgr2v2e  29506  umgr2v2enb1  29507  umgr2v2evd2  29508  vdegp1ai  29517  vdegp1bi  29518  wlk2v2elem2  30138  wlk2v2e  30139  eupth2lems  30220  frcond2  30249  frcond3  30251  nfrgr2v  30254  frgr3vlem1  30255  frgr3vlem2  30256  frgrncvvdeqlem2  30282  ex-uni  30408  ex-eprel  30415  indf1ofs  32854  idlsrgval  33475  constr0  33771  prsiga  34165  difelsiga  34167  measssd  34249  carsgsigalem  34349  carsgclctun  34355  pmeasmono  34358  eulerpartlemn  34415  probun  34453  coinflipprob  34514  coinflipspace  34515  coinfliprv  34517  coinflippv  34518  cusgredgex  35187  subfacp1lem3  35247  subfacp1lem5  35249  ex-sategoelel12  35492  altopex  36025  altopthsn  36026  altxpsspw  36042  bj-endval  37380  poimirlem9  37689  poimirlem15  37695  tgrpset  40864  hlhilset  42053  aprilfools2025  42792  kelac2lem  43181  kelac2  43182  mendval  43296  tr3dom  43645  fvrcllb0d  43810  fvrcllb0da  43811  fvrcllb1d  43812  corclrcl  43824  corcltrcl  43856  cotrclrcl  43859  clsk1indlem2  44159  clsk1indlem3  44160  clsk1indlem4  44161  clsk1indlem1  44162  mnuprdlem3  44391  mnurndlem1  44398  permaxpr  45127  prsal  46440  sge0pr  46516  elsprel  47599  sprvalpw  47604  prprvalpw  47639  sbcpr  47645  nnsum3primes4  47912  nnsum3primesgbe  47916  opstrgric  48050  stgrfv  48077  stgredgel  48081  usgrexmpl1lem  48145  usgrexmpl1edg  48148  usgrexmpl1tri  48149  usgrexmpl2lem  48150  usgrexmpl2edg  48153  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2nb4  48159  usgrexmpl2nb5  48160  usgrexmpl2trifr  48161  gpgov  48166  gpgvtx  48167  gpgiedg  48168  gpgiedgdmellem  48170  gpgprismgr4cycllem2  48220  gpgprismgr4cycllem3  48221  gpgprismgr4cycllem8  48226  gpgprismgr4cycllem10  48228  pgnbgreunbgr  48249  fprmappr  48469  zlmodzxzlmod  48478  zlmodzxzel  48479  zlmodzxz0  48480  zlmodzxzscm  48481  zlmodzxzadd  48482  zlmodzxzldeplem1  48625  zlmodzxzldeplem3  48627  zlmodzxzldeplem4  48628  ldepsnlinclem1  48630  ldepsnlinclem2  48631  ldepsnlinc  48633  2arymaptfo  48779  prelrrx2  48838  rrx2xpref1o  48843  rrx2plordisom  48848  ehl2eudisval0  48850  rrx2linesl  48868  2sphere0  48875  line2  48877  line2x  48879  line2y  48880  resipos  49099  fucoppcffth  49536  termc2  49643  uobeqterm  49671  incat  49726  onsetreclem1  49830