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

Theorem snex 5297
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 5249. (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 4538 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4631 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 570 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2874 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 5296 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3515 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6eqeltrid 2894 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4613 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 219 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 5175 . . 3 ∅ ∈ V
119, 10eqeltrdi 2898 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 185 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1538  wcel 2111  Vcvv 3441  c0 4243  {csn 4525  {cpr 4527
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 2113  ax-9 2121  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295
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 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-nul 4244  df-sn 4526  df-pr 4528
This theorem is referenced by:  prex  5298  sels  5299  elALT  5300  dtruALT2  5301  snelpwi  5302  snelpw  5303  rext  5306  sspwb  5307  intid  5315  moabex  5316  nnullss  5319  exss  5320  elopg  5323  opi1  5325  op1stb  5328  opnz  5330  opeqsng  5358  opeqpr  5360  snopeqop  5361  opthwiener  5369  uniop  5370  0sn0ep  5434  frirr  5496  opthprc  5580  frsn  5603  xpsspw  5646  relop  5685  snsn0non  6277  onnev  6279  onnevOLD  6280  funopg  6358  funsneqopb  6891  fsnex  7017  tpex  7450  snnex  7460  difsnexi  7463  sucexb  7504  soex  7608  elxp4  7609  elxp5  7610  fvclex  7642  opabex3d  7648  opabex3rd  7649  opabex3  7650  1stval  7673  2ndval  7674  fo1st  7691  fo2nd  7692  mpoexxg  7756  cnvf1o  7789  fnse  7810  suppsnop  7827  brtpos2  7881  wfrlem15  7952  tfrlem12  8008  tfrlem16  8012  mapsnd  8433  fvdiagfn  8438  mapsnconst  8439  mapsncnv  8440  mapsnf1o2  8441  ralxpmap  8443  elixpsn  8484  ixpsnf1o  8485  mapsnf1o  8486  ensn1  8556  en1b  8560  2dom  8565  mapsnend  8571  snmapen  8573  xpsnen  8584  endisj  8587  xpsnen2g  8593  domunsncan  8600  enfixsn  8609  domunsn  8651  fodomr  8652  disjenex  8659  domssex2  8661  domssex  8662  map2xp  8671  phplem2  8681  isinf  8715  pssnn  8720  findcard2  8742  ac6sfi  8746  xpfi  8773  fodomfi  8781  pwfilem  8802  fczfsuppd  8835  snopfsupp  8840  fisn  8875  marypha1lem  8881  brwdom2  9021  unxpwdom2  9036  elirrv  9044  epfrs  9157  tc2  9168  tcsni  9169  ranksuc  9278  djuex  9321  fseqenlem1  9435  dfac5lem2  9535  dfac5lem3  9536  dfac5lem4  9537  kmlem2  9562  djuassen  9589  mapdjuen  9591  djudom1  9593  djuinf  9599  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  11891  hashxplem  13790  hashmap  13792  hashbclem  13806  hashf1lem1  13809  hashge3el3dif  13840  ofs1  14321  climconst2  14897  incexclem  15183  ramub1lem2  16353  cshwsex  16426  setsvalg  16504  setsid  16530  pwsbas  16752  pwsle  16757  pwssca  16761  pwssnf1o  16763  imasplusg  16782  imasmulr  16783  imasvsca  16785  imasip  16786  acsfn  16922  isfunc  17126  homaf  17282  homaval  17283  funcsetcestrclem1  17396  mgm1  17860  sgrp1  17902  mnd1  17944  mnd1id  17945  efmnd1bas  18050  idresefmnd  18056  smndex1bas  18063  smndex1sgrp  18065  smndex1mnd  18067  smndex1id  18068  grp1  18198  grp1inv  18199  mulgfval  18218  triv1nsgd  18317  1nsgtrivd  18318  symg2bas  18513  symgvalstruct  18517  idrespermg  18531  pmtrsn  18639  psgnsn  18640  abl1  18979  gsum2d2  19087  gsumcom2  19088  dprdz  19145  dprdsn  19151  dprd2da  19157  simpgnsgd  19215  2nsgsimpgd  19217  ring1  19348  pwssplit3  19826  rng1nnzr  20040  frlmip  20467  islindf4  20527  evlssca  20761  mpfind  20779  evls1sca  20947  pf1ind  20979  mattposvs  21060  mat1dimelbas  21076  mat1dimscm  21080  mat1dimmul  21081  mat1rhmval  21084  m1detdiag  21202  mdetrlin  21207  mdetrsca2  21209  mdetrlin2  21212  mdetunilem5  21221  smadiadetglem2  21277  basdif0  21558  ordtbas  21797  leordtval2  21817  dishaus  21987  discmp  22003  conncompid  22036  dis2ndc  22065  dislly  22102  dis1stc  22104  unisngl  22132  1stckgen  22159  ptbasfi  22186  dfac14lem  22222  dfac14  22223  ptrescn  22244  xkoptsub  22259  pt1hmeo  22411  xpstopnlem1  22414  ptcmpfi  22418  isufil2  22513  ufileu  22524  filufint  22525  uffix  22526  uffixsn  22530  flimclslem  22589  ptcmplem1  22657  cnextfval  22667  imasdsf1olem  22980  icccmplem1  23427  icccmplem2  23428  rrxip  23994  rrxsca  24000  ehl1eudis  24024  elply2  24793  plyss  24796  plyeq0lem  24807  taylfval  24954  axlowdimlem15  26750  axlowdim  26755  snstriedgval  26831  vtxvalsnop  26834  iedgvalsnop  26835  upgr1eop  26908  upgr1eopALT  26910  uspgr1eop  27037  usgr1eop  27040  lfuhgr1v0e  27044  1loopgrvd2  27293  1loopgrvd0  27294  p1evtxdeqlem  27302  p1evtxdeq  27303  p1evtxdp1  27304  uspgrloopvtx  27305  uspgrloopiedg  27307  uspgrloopedg  27308  wlkp1lem4  27466  0pthonv  27914  eupth2lem3  28021  wlkl0  28152  0ofval  28570  suppovss  30443  resf1o  30492  gsumpart  30740  zar0ring  31231  ordtconnlem1  31277  esumpr  31435  esumrnmpt2  31437  esumfzf  31438  esum2dlem  31461  esum2d  31462  esumiun  31463  prsiga  31500  rossros  31549  cntnevol  31597  carsgclctunlem1  31685  omsmeas  31691  eulerpartlemgs2  31748  ccatmulgnn0dir  31922  ofcs1  31924  actfunsnf1o  31985  actfunsnrndisj  31986  reprsuc  31996  breprexplema  32011  bnj918  32147  bnj95  32246  bnj1452  32434  bnj1489  32438  subfacp1lem5  32544  erdszelem5  32555  erdszelem8  32558  cvmliftlem4  32648  cvmliftlem5  32649  cvmlift2lem6  32668  cvmlift2lem9  32671  cvmlift2lem12  32674  satfv1lem  32722  prv1n  32791  frrlem13  33248  conway  33377  etasslt  33387  slerec  33390  fobigcup  33474  elsingles  33492  fnsingle  33493  fvsingle  33494  dfiota3  33497  brapply  33512  brsuccf  33515  funpartlem  33516  altopthsn  33535  altxpsspw  33551  hfsn  33753  neibastop2lem  33821  topjoin  33826  onpsstopbas  33891  bj-snsetex  34399  bj-elsngl  34404  bj-2uplex  34458  bj-restsn  34497  f1omptsnlem  34753  mptsnunlem  34755  topdifinffinlem  34764  finixpnum  35042  ptrest  35056  poimirlem3  35060  poimirlem4  35061  poimirlem28  35085  fdc  35183  heiborlem3  35251  heiborlem8  35256  ismrer1  35276  grposnOLD  35320  zrdivrng  35391  ecexALTV  35748  eccnvepex  35752  ldualset  36421  lineset  37034  ispointN  37038  dvaset  38301  dvhset  38377  dibval  38438  dibfna  38450  frlmsnic  39451  elrfi  39633  mzpincl  39673  mzpcompact2lem  39690  wopprc  39969  dfac11  40004  kelac2  40007  pwslnmlem1  40034  pwslnm  40036  sn1dom  40232  pr2dom  40233  tr3dom  40234  fvilbdRP  40389  brtrclfv2  40426  frege110  40672  frege133  40695  k0004lem3  40850  mnuprdlem1  40978  mnuprdlem2  40979  snelpwrVD  41535  fnchoice  41656  mpct  41828  elmapsnd  41831  difmapsn  41839  unirnmapsn  41841  ssmapsn  41843  limcresiooub  42282  limcresioolb  42283  cnfdmsn  42522  dvsinax  42553  fourierdlem48  42794  fourierdlem49  42795  salexct3  42980  salgencntex  42981  salgensscntex  42982  sge0sn  43016  sge0p1  43051  sge0xp  43066  ovnovollem1  43293  ovnovollem2  43294  vonvolmbllem  43297  setsv  43893  nnsum3primesprm  44306  mpoexxg2  44737  mapsnop  44744  lindsrng01  44875  snlindsntorlem  44877  snlindsntor  44878  lmod1lem1  44894  lmod1lem2  44895  lmod1lem3  44896  lmod1lem4  44897  lmod1lem5  44898  lmod1  44899  lmod1zr  44900  fv1arycl  45049  1arympt1fv  45051  1arymaptfo  45055  aacllem  45327
  Copyright terms: Public domain W3C validator