Theorem prex 5379

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 4721), 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 4688	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2813	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5375	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3511	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4687	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2813	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3510	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4719	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5378	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2836	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4720	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5378	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2836	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2109  Vcvv 3438  {csn 4579  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-un 3910  df-nul 4287  df-sn 4580  df-pr 4582

This theorem is referenced by:  prelpw  5393  opex  5411  elopg  5413  opi2  5416  op1stb  5418  opth  5423  opeqsng  5450  opeqpr  5452  opthwiener  5461  uniop  5462  opthhausdorff  5464  opthhausdorff0  5465  fr2nr  5600  xpsspw  5756  relop  5797  f1prex  7225  unexg  7683  unexOLD  7685  tpex  7686  2oex  8406  en2prd  8980  pw2f1olem  9005  dif1en  9084  dif1enOLD  9086  opthreg  9533  djuexALT  9837  dfac2b  10044  intwun  10648  wunex2  10651  wuncval2  10660  intgru  10727  xrex  12906  seqexw  13942  pr2pwpr  14404  wwlktovfo  14883  prmreclem2  16847  prdsval  17377  xpsfval  17488  xpssca  17498  xpsvsca  17499  isposix  18248  clatl  18432  ipoval  18454  mgm0b  18549  frmdval  18743  mgmnsgrpex  18823  sgrpnmndex  18824  symg2bas  19290  pmtrprfval  19384  pmtrprfvalrn  19385  psgnprfval1  19419  psgnprfval2  19420  isnzr2hash  20422  psgnghm  21505  psgnco  21508  evpmodpmf1o  21521  mdetralt  22511  m2detleiblem5  22528  m2detleiblem6  22529  m2detleiblem3  22532  m2detleiblem4  22533  m2detleib  22534  indistopon  22904  pptbas  22911  indistpsALT  22916  tuslem  24170  tmslem  24386  ehl2eudis  25338  sqff1o  27108  dchrval  27161  elno  27573  eengv  28942  structvtxvallem  28983  structiedg0val  28985  upgrbi  29056  umgrbi  29064  upgr1e  29076  umgredg  29101  uspgr1e  29207  usgr1e  29208  uspgr1ewop  29211  uspgr2v1e2w  29214  usgr2v1e2w  29215  usgrexmplef  29222  usgrexmpledg  29225  1loopgrnb0  29466  1egrvtxdg1  29473  1egrvtxdg0  29475  umgr2v2evtx  29485  umgr2v2eiedg  29487  umgr2v2e  29489  umgr2v2enb1  29490  umgr2v2evd2  29491  vdegp1ai  29500  vdegp1bi  29501  wlk2v2elem2  30118  wlk2v2e  30119  eupth2lems  30200  frcond2  30229  frcond3  30231  nfrgr2v  30234  frgr3vlem1  30235  frgr3vlem2  30236  frgrncvvdeqlem2  30262  ex-uni  30388  ex-eprel  30395  indf1ofs  32822  idlsrgval  33450  constr0  33703  prsiga  34097  difelsiga  34099  measssd  34181  carsgsigalem  34282  carsgclctun  34288  pmeasmono  34291  eulerpartlemn  34348  probun  34386  coinflipprob  34447  coinflipspace  34448  coinfliprv  34450  coinflippv  34451  cusgredgex  35094  subfacp1lem3  35154  subfacp1lem5  35156  ex-sategoelel12  35399  altopex  35933  altopthsn  35934  altxpsspw  35950  bj-endval  37288  poimirlem9  37608  poimirlem15  37614  tgrpset  40724  hlhilset  41913  aprilfools2025  42647  kelac2lem  43037  kelac2  43038  mendval  43152  tr3dom  43501  fvrcllb0d  43666  fvrcllb0da  43667  fvrcllb1d  43668  corclrcl  43680  corcltrcl  43712  cotrclrcl  43715  clsk1indlem2  44015  clsk1indlem3  44016  clsk1indlem4  44017  clsk1indlem1  44018  mnuprdlem3  44247  mnurndlem1  44254  permaxpr  44984  prsal  46300  sge0pr  46376  elsprel  47460  sprvalpw  47465  prprvalpw  47500  sbcpr  47506  nnsum3primes4  47773  nnsum3primesgbe  47777  opstrgric  47911  stgrfv  47938  stgredgel  47942  usgrexmpl1lem  48006  usgrexmpl1edg  48009  usgrexmpl1tri  48010  usgrexmpl2lem  48011  usgrexmpl2edg  48014  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2nb4  48020  usgrexmpl2nb5  48021  usgrexmpl2trifr  48022  gpgov  48027  gpgvtx  48028  gpgiedg  48029  gpgiedgdmellem  48031  gpgprismgr4cycllem2  48081  gpgprismgr4cycllem3  48082  gpgprismgr4cycllem8  48087  gpgprismgr4cycllem10  48089  pgnbgreunbgr  48110  fprmappr  48330  zlmodzxzlmod  48339  zlmodzxzel  48340  zlmodzxz0  48341  zlmodzxzscm  48342  zlmodzxzadd  48343  zlmodzxzldeplem1  48486  zlmodzxzldeplem3  48488  zlmodzxzldeplem4  48489  ldepsnlinclem1  48491  ldepsnlinclem2  48492  ldepsnlinc  48494  2arymaptfo  48640  prelrrx2  48699  rrx2xpref1o  48704  rrx2plordisom  48709  ehl2eudisval0  48711  rrx2linesl  48729  2sphere0  48736  line2  48738  line2x  48740  line2y  48741  resipos  48960  fucoppcffth  49397  termc2  49504  uobeqterm  49532  incat  49587  onsetreclem1  49691