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

Theorem snex 4835
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4778. (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 4138 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4214 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 675 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2672 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 4834 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3239 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6syl5eqel 2692 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4197 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 205 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 4718 . . 3 ∅ ∈ V
119, 10syl6eqel 2696 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 175 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1475  wcel 1977  Vcvv 3173  c0 3874  {csn 4125  {cpr 4127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-un 3545  df-nul 3875  df-sn 4126  df-pr 4128
This theorem is referenced by:  prex  4836  elALT  4837  dtruALT2  4838  snelpwi  4839  snelpw  4840  rext  4843  sspwb  4844  intid  4853  moabex  4854  nnullss  4857  exss  4858  elopg  4861  opi1  4864  op1stb  4867  opnz  4868  opeqsn  4892  opeqpr  4893  propssopi  4896  opthwiener  4901  uniop  4902  frirr  5015  frsn  5112  xpsspw  5156  relop  5194  onnev  5765  funopg  5836  funsneqopsn  6322  funsneqop  6323  fsnex  6438  tpex  6855  snnex  6862  difsnexi  6864  sucexb  6901  soex  7002  elxp4  7003  elxp5  7004  opabex3d  7037  opabex3  7038  1stval  7061  2ndval  7062  fo1st  7079  fo2nd  7080  mpt2exxg  7133  cnvf1o  7163  fnse  7181  suppsnop  7196  brtpos2  7245  wfrlem15  7316  tfrlem12  7372  tfrlem16  7376  mapsn  7785  fvdiagfn  7788  mapsnconst  7789  mapsncnv  7790  mapsnf1o2  7791  ralxpmap  7793  elixpsn  7833  ixpsnf1o  7834  mapsnf1o  7835  ensn1  7906  en1b  7910  mapsnen  7920  xpsnen  7929  endisj  7932  xpsnen2g  7938  domunsncan  7945  enfixsn  7954  domunsn  7995  fodomr  7996  disjenex  8003  domssex2  8005  domssex  8006  map2xp  8015  phplem2  8025  isinf  8058  pssnn  8063  findcard2  8085  ac6sfi  8089  xpfi  8116  fodomfi  8124  pwfilem  8143  fczfsuppd  8176  snopfsupp  8181  fisn  8216  marypha1lem  8222  brwdom2  8361  unxpwdom2  8376  elirrv  8387  epfrs  8490  tc2  8501  tcsni  8502  ranksuc  8611  fseqenlem1  8730  dfac5lem2  8830  dfac5lem3  8831  dfac5lem4  8832  kmlem2  8856  cdafn  8874  cdaval  8875  cdaassen  8887  mapcdaen  8889  cdadom1  8891  cdainf  8897  ackbij1lem5  8929  cfsuc  8962  isfin1-3  9091  hsmexlem4  9134  axcc2lem  9141  dcomex  9152  axdc3lem4  9158  axdc4lem  9160  ttukeylem3  9216  brdom7disj  9234  brdom6disj  9235  fpwwe2lem13  9343  canthwe  9352  canthp1lem1  9353  uniwun  9441  rankcf  9478  nn0ex  11175  hashxplem  13080  hashmap  13082  hashbclem  13093  hashf1lem1  13096  hashge3el3dif  13122  ofs1  13557  climconst2  14127  incexclem  14407  ramub1lem2  15569  cshwsex  15645  setsvalg  15719  setsid  15742  pwsbas  15970  pwsle  15975  pwssca  15979  pwssnf1o  15981  imasplusg  16000  imasmulr  16001  imasvsca  16003  imasip  16004  xpsc  16040  acsfn  16143  isfunc  16347  homaf  16503  homaval  16504  funcsetcestrclem1  16617  mgm1  17080  sgrp1  17116  mnd1  17154  mnd1id  17155  grp1  17345  grp1inv  17346  symg2bas  17641  idrespermg  17654  pmtrsn  17762  psgnsn  17763  abl1  18092  gsum2d2  18196  gsumcom2  18197  dprdz  18252  dprdsn  18258  dprd2da  18264  ring1  18425  pwssplit3  18882  drngnidl  19050  drnglpir  19074  rng1nnzr  19095  evlssca  19343  mpfind  19357  evls1sca  19509  pf1ind  19540  frlmip  19936  islindf4  19996  mattposvs  20080  mat1dimelbas  20096  mat1dimscm  20100  mat1dimmul  20101  mat1rhmval  20104  m1detdiag  20222  mdetrlin  20227  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  smadiadetglem2  20297  basdif0  20568  ordtbas  20806  leordtval2  20826  dishaus  20996  discmp  21011  concompid  21044  dis2ndc  21073  dislly  21110  dis1stc  21112  unisngl  21140  1stckgen  21167  ptbasfi  21194  dfac14lem  21230  dfac14  21231  ptrescn  21252  xkoptsub  21267  pt1hmeo  21419  xpstopnlem1  21422  ptcmpfi  21426  isufil2  21522  ufileu  21533  filufint  21534  uffix  21535  uffixsn  21539  flimclslem  21598  ptcmplem1  21666  cnextfval  21676  imasdsf1olem  21988  icccmplem1  22433  icccmplem2  22434  rrxip  22986  elply2  23756  plyss  23759  plyeq0lem  23770  taylfval  23917  axlowdimlem15  25636  axlowdim  25641  snstrvtxval  25712  snstriedgval  25713  vtxvalsnop  25716  iedgvalsnop  25717  upgr1eop  25781  upgr1eopALT  25783  umgra1  25855  uslgra1  25901  usgra1  25902  usgra1v  25919  cusgra1v  25990  uvtx01vtx  26020  wlkntrl  26092  0pthonv  26111  constr1trl  26118  1pthon  26121  1pthon2v  26123  1conngra  26203  vdgr1d  26430  vdgr1b  26431  vdgr1a  26433  0ofval  27026  resf1o  28893  ordtconlem1  29298  esumpr  29455  esumrnmpt2  29457  esumfzf  29458  esum2dlem  29481  esum2d  29482  esumiun  29483  prsiga  29521  rossros  29570  cntnevol  29618  carsgclctunlem1  29706  omsmeas  29712  eulerpartlemgs2  29769  ccatmulgnn0dir  29945  ofcs1  29947  bnj918  30090  bnj95  30188  bnj1452  30374  bnj1489  30378  subfacp1lem5  30420  erdszelem5  30431  erdszelem8  30434  cvmliftlem4  30524  cvmliftlem5  30525  cvmlift2lem6  30544  cvmlift2lem9  30547  cvmlift2lem12  30550  fobigcup  31177  elsingles  31195  fnsingle  31196  fvsingle  31197  dfiota3  31200  brapply  31215  brsuccf  31218  funpartlem  31219  altopthsn  31238  altxpsspw  31254  hfsn  31456  neibastop2lem  31525  topjoin  31530  onpsstopbas  31599  bj-sels  32143  bj-snsetex  32144  bj-elsngl  32149  bj-2uplex  32203  bj-restsn  32216  f1omptsnlem  32359  mptsnunlem  32361  topdifinffinlem  32371  finixpnum  32564  ptrest  32578  poimirlem3  32582  poimirlem4  32583  poimirlem28  32607  fdc  32711  heiborlem3  32782  heiborlem8  32787  ismrer1  32807  grposnOLD  32851  zrdivrng  32922  ldualset  33430  lineset  34042  ispointN  34046  dvaset  35311  dvhset  35388  dibval  35449  dibfna  35461  elrfi  36275  mzpincl  36315  mzpcompact2lem  36332  wopprc  36615  dfac11  36650  kelac2  36653  pwslnmlem1  36680  pwslnm  36682  fvilbdRP  37001  brtrclfv2  37038  frege110  37287  frege133  37310  k0004lem3  37467  snelpwrVD  38088  fnchoice  38211  mapsnd  38383  mapsnend  38386  mpct  38388  elmapsnd  38391  difmapsn  38399  unirnmapsn  38401  ssmapsn  38403  limcresiooub  38709  limcresioolb  38710  cnfdmsn  38767  dvsinax  38801  fourierdlem48  39047  fourierdlem49  39048  salexct3  39236  salgencntex  39237  salgensscntex  39238  sge0sn  39272  sge0p1  39307  sge0xp  39322  ovnovollem1  39546  ovnovollem2  39547  vonvolmbllem  39550  nnsum3primesprm  40206  uspgr1eop  40473  usgr1eop  40476  lfuhgr1v0e  40480  1loopgrvd2  40718  1loopgrvd0  40719  p1evtxdeqlem  40728  p1evtxdeq  40729  p1evtxdp1  40730  uspgrloopvtx  40731  uspgrloopiedg  40733  uspgrloopedg  40734  1wlkp1lem4  40885  is01wlk  41285  is0Trl  41291  0pthonv-av  41297  eupth0  41382  eupth2lem3  41404  mpt2exxg2  41909  mapsnop  41916  lindsrng01  42051  snlindsntorlem  42053  snlindsntor  42054  lmod1lem1  42070  lmod1lem2  42071  lmod1lem3  42072  lmod1lem4  42073  lmod1lem5  42074  lmod1  42075  lmod1zr  42076  aacllem  42356
  Copyright terms: Public domain W3C validator