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

Theorem prex 5301
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 4666), 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 4633 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2877 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 5299 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3518 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4632 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2877 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 247 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3532 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4664 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 5300 . . 3 {𝐵} ∈ V
119, 10eqeltrdi 2901 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4665 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 5300 . . 3 {𝐴} ∈ V
1412, 13eqeltrdi 2901 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 187 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1538  wcel 2112  Vcvv 3444  {csn 4528  {cpr 4530
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-dif 3887  df-un 3889  df-nul 4247  df-sn 4529  df-pr 4531
This theorem is referenced by:  prelpw  5307  opex  5324  elopg  5326  opi2  5329  op1stb  5331  opth  5336  opeqsng  5361  opeqpr  5363  opthwiener  5372  uniop  5373  opthhausdorff  5375  opthhausdorff0  5376  fr2nr  5501  xpsspw  5650  relop  5689  f1prex  7022  unex  7453  tpex  7454  pw2f1olem  8608  1sdom  8709  opthreg  9069  djuexALT  9339  pr2ne  9420  dfac2b  9545  intwun  10150  wunex2  10153  wuncval2  10162  intgru  10229  xrex  12378  seqexw  13384  pr2pwpr  13837  wwlktovfo  14317  prmreclem2  16247  prdsval  16724  xpsfval  16835  xpssca  16845  xpsvsca  16846  isposix  17563  clatl  17722  ipoval  17760  mgm0b  17863  frmdval  18012  mgmnsgrpex  18092  sgrpnmndex  18093  symg2bas  18517  pmtrprfval  18611  pmtrprfvalrn  18612  psgnprfval1  18646  psgnprfval2  18647  isnzr2hash  20034  psgnghm  20273  psgnco  20276  evpmodpmf1o  20289  mdetralt  21217  m2detleiblem5  21234  m2detleiblem6  21235  m2detleiblem3  21238  m2detleiblem4  21239  m2detleib  21240  indistopon  21610  pptbas  21617  indistpsALT  21622  tuslem  22877  tmslem  23093  ehl2eudis  24030  sqff1o  25771  dchrval  25822  eengv  26777  structvtxvallem  26817  structiedg0val  26819  upgrbi  26890  umgrbi  26898  upgr1e  26910  umgredg  26935  uspgr1e  27038  usgr1e  27039  uspgr1ewop  27042  uspgr2v1e2w  27045  usgr2v1e2w  27046  usgrexmplef  27053  usgrexmpledg  27056  1loopgrnb0  27296  1egrvtxdg1  27303  1egrvtxdg0  27305  umgr2v2evtx  27315  umgr2v2eiedg  27317  umgr2v2e  27319  umgr2v2enb1  27320  umgr2v2evd2  27321  vdegp1ai  27330  vdegp1bi  27331  wlk2v2elem2  27945  wlk2v2e  27946  eupth2lems  28027  frcond2  28056  frcond3  28058  nfrgr2v  28061  frgr3vlem1  28062  frgr3vlem2  28063  frgrncvvdeqlem2  28089  ex-uni  28215  ex-eprel  28222  idlsrgval  31060  indf1ofs  31399  prsiga  31504  difelsiga  31506  measssd  31588  carsgsigalem  31687  carsgclctun  31693  pmeasmono  31696  eulerpartlemn  31753  probun  31791  coinflipprob  31851  coinflipspace  31852  coinfliprv  31854  coinflippv  31855  cusgredgex  32482  subfacp1lem3  32543  subfacp1lem5  32545  ex-sategoelel12  32788  altopex  33535  altopthsn  33536  altxpsspw  33552  bj-endval  34730  poimirlem9  35065  poimirlem15  35071  tgrpset  38040  hlhilset  39229  kelac2lem  40005  kelac2  40006  mendval  40124  tr3dom  40233  fvrcllb0d  40391  fvrcllb0da  40392  fvrcllb1d  40393  corclrcl  40405  corcltrcl  40437  cotrclrcl  40440  clsk1indlem2  40742  clsk1indlem3  40743  clsk1indlem4  40744  clsk1indlem1  40745  mnuprdlem3  40979  mnurndlem1  40986  prsal  42957  sge0pr  43030  elsprel  43989  sprvalpw  43994  prprvalpw  44029  sbcpr  44035  nnsum3primes4  44303  nnsum3primesgbe  44307  strisomgrop  44355  fprmappr  44744  zlmodzxzlmod  44753  zlmodzxzel  44754  zlmodzxz0  44755  zlmodzxzscm  44756  zlmodzxzadd  44757  zlmodzxzldeplem1  44906  zlmodzxzldeplem3  44908  zlmodzxzldeplem4  44909  ldepsnlinclem1  44911  ldepsnlinclem2  44912  ldepsnlinc  44914  2arymaptfo  45065  prelrrx2  45124  rrx2xpref1o  45129  rrx2plordisom  45134  ehl2eudisval0  45136  rrx2linesl  45154  2sphere0  45161  line2  45163  line2x  45165  line2y  45166  onsetreclem1  45231
  Copyright terms: Public domain W3C validator