Theorem prex 5407

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 4743), 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 4710	. . . . . 6 ⊢ (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
2	1	eleq1d 2819	. . . . 5 ⊢ (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3		zfpair2 5403	. . . . 5 ⊢ {𝑥, 𝑦} ∈ V
4	2, 3	vtoclg 3533	. . . 4 ⊢ (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5		preq1 4709	. . . . 5 ⊢ (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
6	5	eleq1d 2819	. . . 4 ⊢ (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
7	4, 6	imbitrid 244	. . 3 ⊢ (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
8	7	vtocleg 3532	. 2 ⊢ (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9		prprc1 4741	. . 3 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10		snex 5406	. . 3 ⊢ {𝐵} ∈ V
11	9, 10	eqeltrdi 2842	. 2 ⊢ (¬ 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12		prprc2 4742	. . 3 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13		snex 5406	. . 3 ⊢ {𝐴} ∈ V
14	12, 13	eqeltrdi 2842	. 2 ⊢ (¬ 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
15	8, 11, 14	pm2.61nii 184	1 ⊢ {𝐴, 𝐵} ∈ V

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ∈ wcel 2108  Vcvv 3459  {csn 4601  {cpr 4603

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-un 3931  df-nul 4309  df-sn 4602  df-pr 4604

This theorem is referenced by:  prelpw  5421  opex  5439  elopg  5441  opi2  5444  op1stb  5446  opth  5451  opeqsng  5478  opeqpr  5480  opthwiener  5489  uniop  5490  opthhausdorff  5492  opthhausdorff0  5493  fr2nr  5631  xpsspw  5788  relop  5830  f1prex  7276  unexg  7735  unexOLD  7737  tpex  7738  2oex  8489  en2prd  9060  pw2f1olem  9088  dif1en  9172  dif1enOLD  9174  1sdomOLD  9255  opthreg  9630  djuexALT  9934  pr2neOLD  10017  dfac2b  10143  intwun  10747  wunex2  10750  wuncval2  10759  intgru  10826  xrex  13001  seqexw  14033  pr2pwpr  14495  wwlktovfo  14975  prmreclem2  16935  prdsval  17467  xpsfval  17578  xpssca  17588  xpsvsca  17589  isposix  18334  clatl  18516  ipoval  18538  mgm0b  18633  frmdval  18827  mgmnsgrpex  18907  sgrpnmndex  18908  symg2bas  19372  pmtrprfval  19466  pmtrprfvalrn  19467  psgnprfval1  19501  psgnprfval2  19502  isnzr2hash  20477  psgnghm  21538  psgnco  21541  evpmodpmf1o  21554  mdetralt  22544  m2detleiblem5  22561  m2detleiblem6  22562  m2detleiblem3  22565  m2detleiblem4  22566  m2detleib  22567  indistopon  22937  pptbas  22944  indistpsALT  22949  tuslem  24203  tmslem  24419  ehl2eudis  25372  sqff1o  27142  dchrval  27195  elno  27607  eengv  28904  structvtxvallem  28945  structiedg0val  28947  upgrbi  29018  umgrbi  29026  upgr1e  29038  umgredg  29063  uspgr1e  29169  usgr1e  29170  uspgr1ewop  29173  uspgr2v1e2w  29176  usgr2v1e2w  29177  usgrexmplef  29184  usgrexmpledg  29187  1loopgrnb0  29428  1egrvtxdg1  29435  1egrvtxdg0  29437  umgr2v2evtx  29447  umgr2v2eiedg  29449  umgr2v2e  29451  umgr2v2enb1  29452  umgr2v2evd2  29453  vdegp1ai  29462  vdegp1bi  29463  wlk2v2elem2  30083  wlk2v2e  30084  eupth2lems  30165  frcond2  30194  frcond3  30196  nfrgr2v  30199  frgr3vlem1  30200  frgr3vlem2  30201  frgrncvvdeqlem2  30227  ex-uni  30353  ex-eprel  30360  indf1ofs  32789  idlsrgval  33464  constr0  33717  prsiga  34108  difelsiga  34110  measssd  34192  carsgsigalem  34293  carsgclctun  34299  pmeasmono  34302  eulerpartlemn  34359  probun  34397  coinflipprob  34458  coinflipspace  34459  coinfliprv  34461  coinflippv  34462  cusgredgex  35090  subfacp1lem3  35150  subfacp1lem5  35152  ex-sategoelel12  35395  altopex  35924  altopthsn  35925  altxpsspw  35941  bj-endval  37279  poimirlem9  37599  poimirlem15  37605  tgrpset  40710  hlhilset  41899  aprilfools2025  42644  kelac2lem  43035  kelac2  43036  mendval  43150  tr3dom  43499  fvrcllb0d  43664  fvrcllb0da  43665  fvrcllb1d  43666  corclrcl  43678  corcltrcl  43710  cotrclrcl  43713  clsk1indlem2  44013  clsk1indlem3  44014  clsk1indlem4  44015  clsk1indlem1  44016  mnuprdlem3  44246  mnurndlem1  44253  permaxpr  44983  prsal  46295  sge0pr  46371  elsprel  47437  sprvalpw  47442  prprvalpw  47477  sbcpr  47483  nnsum3primes4  47750  nnsum3primesgbe  47754  opstrgric  47887  stgrfv  47913  stgredgel  47917  usgrexmpl1lem  47973  usgrexmpl1edg  47976  usgrexmpl1tri  47977  usgrexmpl2lem  47978  usgrexmpl2edg  47981  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2nb4  47987  usgrexmpl2nb5  47988  usgrexmpl2trifr  47989  gpgov  47994  gpgvtx  47995  gpgiedg  47996  gpgiedgdmellem  47998  gpgprismgr4cycllem2  48043  gpgprismgr4cycllem3  48044  gpgprismgr4cycllem8  48049  gpgprismgr4cycllem10  48051  fprmappr  48268  zlmodzxzlmod  48277  zlmodzxzel  48278  zlmodzxz0  48279  zlmodzxzscm  48280  zlmodzxzadd  48281  zlmodzxzldeplem1  48424  zlmodzxzldeplem3  48426  zlmodzxzldeplem4  48427  ldepsnlinclem1  48429  ldepsnlinclem2  48430  ldepsnlinc  48432  2arymaptfo  48582  prelrrx2  48641  rrx2xpref1o  48646  rrx2plordisom  48651  ehl2eudisval0  48653  rrx2linesl  48671  2sphere0  48678  line2  48680  line2x  48682  line2y  48683  resipos  48897  termc2  49351  incat  49426  onsetreclem1  49517