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

Theorem prex 5388
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 4727), 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 4694 . . . . . 6 (𝑦 = 𝐵 → {𝑥, 𝑦} = {𝑥, 𝐵})
21eleq1d 2823 . . . . 5 (𝑦 = 𝐵 → ({𝑥, 𝑦} ∈ V ↔ {𝑥, 𝐵} ∈ V))
3 zfpair2 5384 . . . . 5 {𝑥, 𝑦} ∈ V
42, 3vtoclg 3524 . . . 4 (𝐵 ∈ V → {𝑥, 𝐵} ∈ V)
5 preq1 4693 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝐵} = {𝐴, 𝐵})
65eleq1d 2823 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝐵} ∈ V ↔ {𝐴, 𝐵} ∈ V))
74, 6syl5ib 244 . . 3 (𝑥 = 𝐴 → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
87vtocleg 3513 . 2 (𝐴 ∈ V → (𝐵 ∈ V → {𝐴, 𝐵} ∈ V))
9 prprc1 4725 . . 3 𝐴 ∈ V → {𝐴, 𝐵} = {𝐵})
10 snex 5387 . . 3 {𝐵} ∈ V
119, 10eqeltrdi 2847 . 2 𝐴 ∈ V → {𝐴, 𝐵} ∈ V)
12 prprc2 4726 . . 3 𝐵 ∈ V → {𝐴, 𝐵} = {𝐴})
13 snex 5387 . . 3 {𝐴} ∈ V
1412, 13eqeltrdi 2847 . 2 𝐵 ∈ V → {𝐴, 𝐵} ∈ V)
158, 11, 14pm2.61nii 184 1 {𝐴, 𝐵} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wcel 2107  Vcvv 3444  {csn 4585  {cpr 4587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pr 5383
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-dif 3912  df-un 3914  df-nul 4282  df-sn 4586  df-pr 4588
This theorem is referenced by:  prelpw  5402  opex  5420  elopg  5422  opi2  5425  op1stb  5427  opth  5432  opeqsng  5458  opeqpr  5460  opthwiener  5469  uniop  5470  opthhausdorff  5472  opthhausdorff0  5473  fr2nr  5609  xpsspw  5762  relop  5803  f1prex  7225  unex  7671  tpex  7672  2oex  8391  en2prd  8926  pw2f1olem  8954  dif1en  9038  dif1enOLD  9040  1sdomOLD  9127  opthreg  9488  djuexALT  9792  pr2neOLD  9875  dfac2b  10000  intwun  10605  wunex2  10608  wuncval2  10617  intgru  10684  xrex  12841  seqexw  13851  pr2pwpr  14306  wwlktovfo  14781  prmreclem2  16724  prdsval  17272  xpsfval  17383  xpssca  17393  xpsvsca  17394  isposix  18149  isposixOLD  18150  clatl  18332  ipoval  18354  mgm0b  18447  frmdval  18596  mgmnsgrpex  18676  sgrpnmndex  18677  symg2bas  19106  pmtrprfval  19201  pmtrprfvalrn  19202  psgnprfval1  19236  psgnprfval2  19237  isnzr2hash  20657  psgnghm  20907  psgnco  20910  evpmodpmf1o  20923  mdetralt  21879  m2detleiblem5  21896  m2detleiblem6  21897  m2detleiblem3  21900  m2detleiblem4  21901  m2detleib  21902  indistopon  22273  pptbas  22280  indistpsALT  22285  indistpsALTOLD  22286  tuslem  23540  tuslemOLD  23541  tmslem  23759  tmslemOLD  23760  ehl2eudis  24708  sqff1o  26453  dchrval  26504  eengv  27714  structvtxvallem  27757  structiedg0val  27759  upgrbi  27830  umgrbi  27838  upgr1e  27850  umgredg  27875  uspgr1e  27978  usgr1e  27979  uspgr1ewop  27982  uspgr2v1e2w  27985  usgr2v1e2w  27986  usgrexmplef  27993  usgrexmpledg  27996  1loopgrnb0  28236  1egrvtxdg1  28243  1egrvtxdg0  28245  umgr2v2evtx  28255  umgr2v2eiedg  28257  umgr2v2e  28259  umgr2v2enb1  28260  umgr2v2evd2  28261  vdegp1ai  28270  vdegp1bi  28271  wlk2v2elem2  28886  wlk2v2e  28887  eupth2lems  28968  frcond2  28997  frcond3  28999  nfrgr2v  29002  frgr3vlem1  29003  frgr3vlem2  29004  frgrncvvdeqlem2  29030  ex-uni  29156  ex-eprel  29163  idlsrgval  32022  indf1ofs  32386  prsiga  32491  difelsiga  32493  measssd  32575  carsgsigalem  32676  carsgclctun  32682  pmeasmono  32685  eulerpartlemn  32742  probun  32780  coinflipprob  32840  coinflipspace  32841  coinfliprv  32843  coinflippv  32844  cusgredgex  33476  subfacp1lem3  33537  subfacp1lem5  33539  ex-sategoelel12  33782  altopex  34431  altopthsn  34432  altxpsspw  34448  bj-endval  35672  poimirlem9  35973  poimirlem15  35979  tgrpset  39094  hlhilset  40283  kelac2lem  41225  kelac2  41226  mendval  41344  tr3dom  41531  fvrcllb0d  41696  fvrcllb0da  41697  fvrcllb1d  41698  corclrcl  41710  corcltrcl  41742  cotrclrcl  41745  clsk1indlem2  42047  clsk1indlem3  42048  clsk1indlem4  42049  clsk1indlem1  42050  mnuprdlem3  42287  mnurndlem1  42294  prsal  44269  sge0pr  44343  elsprel  45367  sprvalpw  45372  prprvalpw  45407  sbcpr  45413  nnsum3primes4  45680  nnsum3primesgbe  45684  strisomgrop  45732  fprmappr  46121  zlmodzxzlmod  46130  zlmodzxzel  46131  zlmodzxz0  46132  zlmodzxzscm  46133  zlmodzxzadd  46134  zlmodzxzldeplem1  46281  zlmodzxzldeplem3  46283  zlmodzxzldeplem4  46284  ldepsnlinclem1  46286  ldepsnlinclem2  46287  ldepsnlinc  46289  2arymaptfo  46440  prelrrx2  46499  rrx2xpref1o  46504  rrx2plordisom  46509  ehl2eudisval0  46511  rrx2linesl  46529  2sphere0  46536  line2  46538  line2x  46540  line2y  46541  onsetreclem1  46849
  Copyright terms: Public domain W3C validator