MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prex Structured version   Visualization version   GIF version

Theorem prex 5389
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 4728), 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.
StepHypRef Expression
1 preq2 4695 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2822 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 5385 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3525 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4694 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2822 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6imbitrid 243 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3514 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4726 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 5388 . . 3 {𝐵} ∈ V
119, 10eqeltrdi 2846 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4727 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 5388 . . 3 {𝐴} ∈ V
1412, 13eqeltrdi 2846 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 184 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1541  wcel 2106  Vcvv 3445  {csn 4586  {cpr 4588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-dif 3913  df-un 3915  df-nul 4283  df-sn 4587  df-pr 4589
This theorem is referenced by:  prelpw  5403  opex  5421  elopg  5423  opi2  5426  op1stb  5428  opth  5433  opeqsng  5460  opeqpr  5462  opthwiener  5471  uniop  5472  opthhausdorff  5474  opthhausdorff0  5475  fr2nr  5611  xpsspw  5765  relop  5806  f1prex  7230  unex  7680  tpex  7681  2oex  8423  en2prd  8992  pw2f1olem  9020  dif1en  9104  dif1enOLD  9106  1sdomOLD  9193  opthreg  9554  djuexALT  9858  pr2neOLD  9941  dfac2b  10066  intwun  10671  wunex2  10674  wuncval2  10683  intgru  10750  xrex  12912  seqexw  13922  pr2pwpr  14378  wwlktovfo  14847  prmreclem2  16789  prdsval  17337  xpsfval  17448  xpssca  17458  xpsvsca  17459  isposix  18214  isposixOLD  18215  clatl  18397  ipoval  18419  mgm0b  18512  frmdval  18661  mgmnsgrpex  18741  sgrpnmndex  18742  symg2bas  19174  pmtrprfval  19269  pmtrprfvalrn  19270  psgnprfval1  19304  psgnprfval2  19305  isnzr2hash  20734  psgnghm  20984  psgnco  20987  evpmodpmf1o  21000  mdetralt  21957  m2detleiblem5  21974  m2detleiblem6  21975  m2detleiblem3  21978  m2detleiblem4  21979  m2detleib  21980  indistopon  22351  pptbas  22358  indistpsALT  22363  indistpsALTOLD  22364  tuslem  23618  tuslemOLD  23619  tmslem  23837  tmslemOLD  23838  ehl2eudis  24786  sqff1o  26531  dchrval  26582  eengv  27928  structvtxvallem  27971  structiedg0val  27973  upgrbi  28044  umgrbi  28052  upgr1e  28064  umgredg  28089  uspgr1e  28192  usgr1e  28193  uspgr1ewop  28196  uspgr2v1e2w  28199  usgr2v1e2w  28200  usgrexmplef  28207  usgrexmpledg  28210  1loopgrnb0  28450  1egrvtxdg1  28457  1egrvtxdg0  28459  umgr2v2evtx  28469  umgr2v2eiedg  28471  umgr2v2e  28473  umgr2v2enb1  28474  umgr2v2evd2  28475  vdegp1ai  28484  vdegp1bi  28485  wlk2v2elem2  29100  wlk2v2e  29101  eupth2lems  29182  frcond2  29211  frcond3  29213  nfrgr2v  29216  frgr3vlem1  29217  frgr3vlem2  29218  frgrncvvdeqlem2  29244  ex-uni  29370  ex-eprel  29377  idlsrgval  32245  indf1ofs  32625  prsiga  32730  difelsiga  32732  measssd  32814  carsgsigalem  32915  carsgclctun  32921  pmeasmono  32924  eulerpartlemn  32981  probun  33019  coinflipprob  33079  coinflipspace  33080  coinfliprv  33082  coinflippv  33083  cusgredgex  33715  subfacp1lem3  33776  subfacp1lem5  33778  ex-sategoelel12  34021  altopex  34545  altopthsn  34546  altxpsspw  34562  bj-endval  35786  poimirlem9  36087  poimirlem15  36093  tgrpset  39208  hlhilset  40397  kelac2lem  41377  kelac2  41378  mendval  41496  tr3dom  41790  fvrcllb0d  41955  fvrcllb0da  41956  fvrcllb1d  41957  corclrcl  41969  corcltrcl  42001  cotrclrcl  42004  clsk1indlem2  42304  clsk1indlem3  42305  clsk1indlem4  42306  clsk1indlem1  42307  mnuprdlem3  42544  mnurndlem1  42551  prsal  44549  sge0pr  44625  elsprel  45657  sprvalpw  45662  prprvalpw  45697  sbcpr  45703  nnsum3primes4  45970  nnsum3primesgbe  45974  strisomgrop  46022  fprmappr  46411  zlmodzxzlmod  46420  zlmodzxzel  46421  zlmodzxz0  46422  zlmodzxzscm  46423  zlmodzxzadd  46424  zlmodzxzldeplem1  46571  zlmodzxzldeplem3  46573  zlmodzxzldeplem4  46574  ldepsnlinclem1  46576  ldepsnlinclem2  46577  ldepsnlinc  46579  2arymaptfo  46730  prelrrx2  46789  rrx2xpref1o  46794  rrx2plordisom  46799  ehl2eudisval0  46801  rrx2linesl  46819  2sphere0  46826  line2  46828  line2x  46830  line2y  46831  onsetreclem1  47140
  Copyright terms: Public domain W3C validator