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

Theorem snex 4829
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4772. (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 4137 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4213 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 674 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2671 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 4828 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3238 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6syl5eqel 2691 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4196 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 204 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 4712 . . 3 ∅ ∈ V
119, 10syl6eqel 2695 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 174 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1474  wcel 1976  Vcvv 3172  c0 3873  {csn 4124  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-un 3544  df-nul 3874  df-sn 4125  df-pr 4127
This theorem is referenced by:  prex  4830  elALT  4831  dtruALT2  4832  snelpwi  4833  snelpw  4834  rext  4836  sspwb  4837  intid  4846  moabex  4847  nnullss  4850  exss  4851  elopg  4854  opi1  4857  op1stb  4860  opnz  4861  opeqsn  4885  opeqpr  4886  opthwiener  4891  uniop  4892  frirr  5004  frsn  5101  xpsspw  5144  relop  5181  onnev  5750  funopg  5821  fsnex  6415  tpex  6832  snnex  6839  difsnexi  6841  sucexb  6878  soex  6979  elxp4  6980  elxp5  6981  opabex3d  7014  opabex3  7015  1stval  7038  2ndval  7039  fo1st  7056  fo2nd  7057  mpt2exxg  7110  cnvf1o  7140  fnse  7158  suppsnop  7173  brtpos2  7222  wfrlem15  7293  tfrlem12  7349  tfrlem16  7353  mapsn  7762  fvdiagfn  7765  mapsnconst  7766  mapsncnv  7767  mapsnf1o2  7768  ralxpmap  7770  elixpsn  7810  ixpsnf1o  7811  mapsnf1o  7812  ensn1  7883  en1b  7887  mapsnen  7897  xpsnen  7906  endisj  7909  xpsnen2g  7915  domunsncan  7922  enfixsn  7931  domunsn  7972  fodomr  7973  disjenex  7980  domssex2  7982  domssex  7983  map2xp  7992  phplem2  8002  isinf  8035  pssnn  8040  findcard2  8062  ac6sfi  8066  xpfi  8093  fodomfi  8101  pwfilem  8120  fczfsuppd  8153  snopfsupp  8158  fisn  8193  marypha1lem  8199  brwdom2  8338  unxpwdom2  8353  elirrv  8364  epfrs  8467  tc2  8478  tcsni  8479  ranksuc  8588  fseqenlem1  8707  dfac5lem2  8807  dfac5lem3  8808  dfac5lem4  8809  kmlem2  8833  cdafn  8851  cdaval  8852  cdaassen  8864  mapcdaen  8866  cdadom1  8868  cdainf  8874  ackbij1lem5  8906  cfsuc  8939  isfin1-3  9068  hsmexlem4  9111  axcc2lem  9118  dcomex  9129  axdc3lem4  9135  axdc4lem  9137  ttukeylem3  9193  brdom7disj  9211  brdom6disj  9212  fpwwe2lem13  9320  canthwe  9329  canthp1lem1  9330  uniwun  9418  rankcf  9455  nn0ex  11147  hashxplem  13034  hashmap  13036  hashbclem  13047  hashf1lem1  13050  hashge3el3dif  13074  ofs1  13505  climconst2  14075  incexclem  14355  ramub1lem2  15517  cshwsex  15593  setsvalg  15667  setsid  15690  pwsbas  15918  pwsle  15923  pwssca  15927  pwssnf1o  15929  imasplusg  15948  imasmulr  15949  imasvsca  15951  imasip  15952  xpsc  15988  acsfn  16091  isfunc  16295  homaf  16451  homaval  16452  funcsetcestrclem1  16565  mgm1  17028  sgrp1  17064  mnd1  17102  mnd1id  17103  grp1  17293  grp1inv  17294  symg2bas  17589  idrespermg  17602  pmtrsn  17710  psgnsn  17711  abl1  18040  gsum2d2  18144  gsumcom2  18145  dprdz  18200  dprdsn  18206  dprd2da  18212  ring1  18373  pwssplit3  18830  drngnidl  18998  drnglpir  19022  rng1nnzr  19043  evlssca  19291  mpfind  19305  evls1sca  19457  pf1ind  19488  frlmip  19883  islindf4  19943  mattposvs  20027  mat1dimelbas  20043  mat1dimscm  20047  mat1dimmul  20048  mat1rhmval  20051  m1detdiag  20169  mdetrlin  20174  mdetrsca2  20176  mdetrlin2  20179  mdetunilem5  20188  smadiadetglem2  20244  basdif0  20515  ordtbas  20753  leordtval2  20773  dishaus  20943  discmp  20958  concompid  20991  dis2ndc  21020  dislly  21057  dis1stc  21059  unisngl  21087  1stckgen  21114  ptbasfi  21141  dfac14lem  21177  dfac14  21178  ptrescn  21199  xkoptsub  21214  pt1hmeo  21366  xpstopnlem1  21369  ptcmpfi  21373  isufil2  21469  ufileu  21480  filufint  21481  uffix  21482  uffixsn  21486  flimclslem  21545  ptcmplem1  21613  cnextfval  21623  imasdsf1olem  21935  icccmplem1  22380  icccmplem2  22381  rrxip  22930  elply2  23700  plyss  23703  plyeq0lem  23714  taylfval  23861  axlowdimlem15  25581  axlowdim  25586  umgra1  25648  uslgra1  25694  usgra1  25695  usgra1v  25712  cusgra1v  25783  uvtx01vtx  25813  wlkntrl  25885  0pthonv  25904  constr1trl  25911  1pthon  25914  1pthon2v  25916  1conngra  25996  vdgr1d  26223  vdgr1b  26224  vdgr1a  26226  0ofval  26819  resf1o  28686  ordtconlem1  29091  esumpr  29248  esumrnmpt2  29250  esumfzf  29251  esum2dlem  29274  esum2d  29275  esumiun  29276  prsiga  29314  rossros  29363  cntnevol  29411  carsgclctunlem1  29499  omsmeas  29505  eulerpartlemgs2  29562  ccatmulgnn0dir  29738  ofcs1  29740  bnj918  29883  bnj95  29981  bnj1452  30167  bnj1489  30171  subfacp1lem5  30213  erdszelem5  30224  erdszelem8  30227  cvmliftlem4  30317  cvmliftlem5  30318  cvmlift2lem6  30337  cvmlift2lem9  30340  cvmlift2lem12  30343  fobigcup  30970  elsingles  30988  fnsingle  30989  fvsingle  30990  dfiota3  30993  brapply  31008  brsuccf  31011  funpartlem  31012  altopthsn  31031  altxpsspw  31047  hfsn  31249  neibastop2lem  31318  topjoin  31323  onpsstopbas  31392  bj-sels  31926  bj-snsetex  31927  bj-elsngl  31932  bj-2uplex  31986  bj-restsn  31999  f1omptsnlem  32142  mptsnunlem  32144  topdifinffinlem  32154  finixpnum  32347  ptrest  32361  poimirlem3  32365  poimirlem4  32366  poimirlem28  32390  fdc  32494  heiborlem3  32565  heiborlem8  32570  ismrer1  32590  grposnOLD  32634  zrdivrng  32705  ldualset  33213  lineset  33825  ispointN  33829  dvaset  35094  dvhset  35171  dibval  35232  dibfna  35244  elrfi  36058  mzpincl  36098  mzpcompact2lem  36115  wopprc  36398  dfac11  36433  kelac2  36436  pwslnmlem1  36463  pwslnm  36465  fvilbdRP  36784  brtrclfv2  36821  frege110  37070  frege133  37093  k0004lem3  37250  snelpwrVD  37871  fnchoice  37994  mapsnd  38166  mapsnend  38169  mpct  38171  elmapsnd  38174  difmapsn  38182  unirnmapsn  38184  ssmapsn  38186  limcresiooub  38492  limcresioolb  38493  cnfdmsn  38550  dvsinax  38584  fourierdlem48  38830  fourierdlem49  38831  salexct3  39019  salgencntex  39020  salgensscntex  39021  sge0sn  39055  sge0p1  39090  sge0xp  39105  ovnovollem1  39329  ovnovollem2  39330  vonvolmbllem  39333  nnsum3primesprm  39990  propssopi  40106  funsneqopsn  40128  funsneqop  40129  snstrvtxval  40249  snstriedgval  40250  vtxvalsnop  40253  iedgvalsnop  40254  upgr1eop  40321  upgr1eopALT  40323  uspgr1eop  40454  usgr1eop  40457  lfuhgr1v0e  40461  1loopgrvd2  40699  1loopgrvd0  40700  p1evtxdeqlem  40709  p1evtxdeq  40710  p1evtxdp1  40711  uspgrloopvtx  40712  uspgrloopiedg  40714  uspgrloopedg  40715  1wlkp1lem4  40866  is01wlk  41266  is0Trl  41272  0pthonv-av  41278  eupth0  41363  eupth2lem3  41385  mpt2exxg2  41890  mapsnop  41897  lindsrng01  42032  snlindsntorlem  42034  snlindsntor  42035  lmod1lem1  42051  lmod1lem2  42052  lmod1lem3  42053  lmod1lem4  42054  lmod1lem5  42055  lmod1  42056  lmod1zr  42057  aacllem  42298
  Copyright terms: Public domain W3C validator