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

Theorem snex 5323
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5275. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)
Assertion
Ref Expression
snex {𝐴} ∈ V

Proof of Theorem snex
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 dfsn2 4572 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4665 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 567 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2897 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 5322 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3568 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6eqeltrid 2917 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4647 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 217 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 5203 . . 3 ∅ ∈ V
119, 10syl6eqel 2921 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 183 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wcel 2105  Vcvv 3495  c0 4290  {csn 4559  {cpr 4561
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-un 3940  df-nul 4291  df-sn 4560  df-pr 4562
This theorem is referenced by:  prex  5324  sels  5325  elALT  5326  dtruALT2  5327  snelpwi  5328  snelpw  5329  rext  5332  sspwb  5333  intid  5342  moabex  5343  nnullss  5346  exss  5347  elopg  5350  opi1  5352  op1stb  5355  opnz  5357  opeqsng  5385  opeqpr  5387  snopeqop  5388  opthwiener  5396  uniop  5397  0sn0ep  5464  frirr  5526  opthprc  5610  frsn  5633  xpsspw  5676  relop  5715  snsn0non  6303  onnev  6305  funopg  6383  funsneqopb  6907  fsnex  7030  tpex  7458  snnex  7468  difsnexi  7471  sucexb  7512  soex  7614  elxp4  7615  elxp5  7616  fvclex  7651  opabex3d  7657  opabex3rd  7658  opabex3  7659  1stval  7682  2ndval  7683  fo1st  7700  fo2nd  7701  mpoexxg  7764  cnvf1o  7797  fnse  7818  suppsnop  7835  brtpos2  7889  wfrlem15  7960  tfrlem12  8016  tfrlem16  8020  mapsnd  8439  fvdiagfn  8444  mapsnconst  8445  mapsncnv  8446  mapsnf1o2  8447  ralxpmap  8449  elixpsn  8490  ixpsnf1o  8491  mapsnf1o  8492  ensn1  8562  en1b  8566  2dom  8571  mapsnend  8577  snmapen  8579  xpsnen  8590  endisj  8593  xpsnen2g  8599  domunsncan  8606  enfixsn  8615  domunsn  8656  fodomr  8657  disjenex  8664  domssex2  8666  domssex  8667  map2xp  8676  phplem2  8686  isinf  8720  pssnn  8725  findcard2  8747  ac6sfi  8751  xpfi  8778  fodomfi  8786  pwfilem  8807  fczfsuppd  8840  snopfsupp  8845  fisn  8880  marypha1lem  8886  brwdom2  9026  unxpwdom2  9041  elirrv  9049  epfrs  9162  tc2  9173  tcsni  9174  ranksuc  9283  djuex  9326  fseqenlem1  9439  dfac5lem2  9539  dfac5lem3  9540  dfac5lem4  9541  kmlem2  9566  djuassen  9593  mapdjuen  9595  djudom1  9597  djuinf  9603  ackbij1lem5  9635  cfsuc  9668  isfin1-3  9797  hsmexlem4  9840  axcc2lem  9847  dcomex  9858  axdc3lem4  9864  axdc4lem  9866  ttukeylem3  9922  brdom7disj  9942  brdom6disj  9943  fpwwe2lem13  10053  canthwe  10062  canthp1lem1  10063  uniwun  10151  rankcf  10188  nn0ex  11892  hashxplem  13784  hashmap  13786  hashbclem  13800  hashf1lem1  13803  hashge3el3dif  13834  ofs1  14320  climconst2  14895  incexclem  15181  ramub1lem2  16353  cshwsex  16424  setsvalg  16502  setsid  16528  pwsbas  16750  pwsle  16755  pwssca  16759  pwssnf1o  16761  imasplusg  16780  imasmulr  16781  imasvsca  16783  imasip  16784  acsfn  16920  isfunc  17124  homaf  17280  homaval  17281  funcsetcestrclem1  17394  mgm1  17858  sgrp1  17900  mnd1  17942  mnd1id  17943  grp1  18146  grp1inv  18147  mulgfval  18166  triv1nsgd  18265  1nsgtrivd  18266  symg2bas  18457  idrespermg  18470  pmtrsn  18578  psgnsn  18579  abl1  18917  gsum2d2  19025  gsumcom2  19026  dprdz  19083  dprdsn  19089  dprd2da  19095  simpgnsgd  19153  2nsgsimpgd  19155  ring1  19283  pwssplit3  19764  rng1nnzr  19977  evlssca  20232  mpfind  20250  evls1sca  20416  pf1ind  20448  frlmip  20852  islindf4  20912  mattposvs  20994  mat1dimelbas  21010  mat1dimscm  21014  mat1dimmul  21015  mat1rhmval  21018  m1detdiag  21136  mdetrlin  21141  mdetrsca2  21143  mdetrlin2  21146  mdetunilem5  21155  smadiadetglem2  21211  basdif0  21491  ordtbas  21730  leordtval2  21750  dishaus  21920  discmp  21936  conncompid  21969  dis2ndc  21998  dislly  22035  dis1stc  22037  unisngl  22065  1stckgen  22092  ptbasfi  22119  dfac14lem  22155  dfac14  22156  ptrescn  22177  xkoptsub  22192  pt1hmeo  22344  xpstopnlem1  22347  ptcmpfi  22351  isufil2  22446  ufileu  22457  filufint  22458  uffix  22459  uffixsn  22463  flimclslem  22522  ptcmplem1  22590  cnextfval  22600  imasdsf1olem  22912  icccmplem1  23359  icccmplem2  23360  rrxip  23922  rrxsca  23928  ehl1eudis  23952  elply2  24715  plyss  24718  plyeq0lem  24729  taylfval  24876  axlowdimlem15  26670  axlowdim  26675  snstriedgval  26751  vtxvalsnop  26754  iedgvalsnop  26755  upgr1eop  26828  upgr1eopALT  26830  uspgr1eop  26957  usgr1eop  26960  lfuhgr1v0e  26964  1loopgrvd2  27213  1loopgrvd0  27214  p1evtxdeqlem  27222  p1evtxdeq  27223  p1evtxdp1  27224  uspgrloopvtx  27225  uspgrloopiedg  27227  uspgrloopedg  27228  wlkp1lem4  27386  0pthonv  27836  eupth2lem3  27943  wlkl0  28074  0ofval  28492  suppovss  30355  resf1o  30393  ordtconnlem1  31067  esumpr  31225  esumrnmpt2  31227  esumfzf  31228  esum2dlem  31251  esum2d  31252  esumiun  31253  prsiga  31290  rossros  31339  cntnevol  31387  carsgclctunlem1  31475  omsmeas  31481  eulerpartlemgs2  31538  ccatmulgnn0dir  31712  ofcs1  31714  actfunsnf1o  31775  actfunsnrndisj  31776  reprsuc  31786  breprexplema  31801  bnj918  31937  bnj95  32036  bnj1452  32222  bnj1489  32226  subfacp1lem5  32329  erdszelem5  32340  erdszelem8  32343  cvmliftlem4  32433  cvmliftlem5  32434  cvmlift2lem6  32453  cvmlift2lem9  32456  cvmlift2lem12  32459  satfv1lem  32507  prv1n  32576  frrlem13  33033  conway  33162  etasslt  33172  slerec  33175  fobigcup  33259  elsingles  33277  fnsingle  33278  fvsingle  33279  dfiota3  33282  brapply  33297  brsuccf  33300  funpartlem  33301  altopthsn  33320  altxpsspw  33336  hfsn  33538  neibastop2lem  33606  topjoin  33611  onpsstopbas  33676  bj-snsetex  34173  bj-elsngl  34178  bj-2uplex  34232  bj-restsn  34268  f1omptsnlem  34500  mptsnunlem  34502  topdifinffinlem  34511  finixpnum  34759  ptrest  34773  poimirlem3  34777  poimirlem4  34778  poimirlem28  34802  fdc  34903  heiborlem3  34974  heiborlem8  34979  ismrer1  34999  grposnOLD  35043  zrdivrng  35114  ecexALTV  35471  eccnvepex  35475  ldualset  36143  lineset  36756  ispointN  36760  dvaset  38023  dvhset  38099  dibval  38160  dibfna  38172  frlmsnic  39029  elrfi  39171  mzpincl  39211  mzpcompact2lem  39228  wopprc  39507  dfac11  39542  kelac2  39545  pwslnmlem1  39572  pwslnm  39574  sn1dom  39772  pr2dom  39773  tr3dom  39774  fvilbdRP  39915  brtrclfv2  39952  frege110  40199  frege133  40222  k0004lem3  40379  mnuprdlem1  40488  mnuprdlem2  40489  snelpwrVD  41045  fnchoice  41166  mpct  41344  elmapsnd  41347  difmapsn  41355  unirnmapsn  41357  ssmapsn  41359  limcresiooub  41803  limcresioolb  41804  cnfdmsn  42045  dvsinax  42077  fourierdlem48  42320  fourierdlem49  42321  salexct3  42506  salgencntex  42507  salgensscntex  42508  sge0sn  42542  sge0p1  42577  sge0xp  42592  ovnovollem1  42819  ovnovollem2  42820  vonvolmbllem  42823  setsv  43419  nnsum3primesprm  43802  efmnd1bas  43960  idresefmnd  43969  smndex1bas  43976  smndex1sgrp  43978  smndex1mnd  43980  smndex1id  43981  mpoexxg2  44284  mapsnop  44291  lindsrng01  44421  snlindsntorlem  44423  snlindsntor  44424  lmod1lem1  44440  lmod1lem2  44441  lmod1lem3  44442  lmod1lem4  44443  lmod1lem5  44444  lmod1  44445  lmod1zr  44446  aacllem  44800
  Copyright terms: Public domain W3C validator