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

Theorem snex 4899
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4843. (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 4181 . . 3 {𝐴} = {𝐴, 𝐴}
2 preq12 4261 . . . . . 6 ((𝑥 = 𝐴𝑥 = 𝐴) → {𝑥, 𝑥} = {𝐴, 𝐴})
32anidms 676 . . . . 5 (𝑥 = 𝐴 → {𝑥, 𝑥} = {𝐴, 𝐴})
43eleq1d 2684 . . . 4 (𝑥 = 𝐴 → ({𝑥, 𝑥} ∈ V ↔ {𝐴, 𝐴} ∈ V))
5 zfpair2 4898 . . . 4 {𝑥, 𝑥} ∈ V
64, 5vtoclg 3261 . . 3 (𝐴 ∈ V → {𝐴, 𝐴} ∈ V)
71, 6syl5eqel 2703 . 2 (𝐴 ∈ V → {𝐴} ∈ V)
8 snprc 4244 . . . 4 𝐴 ∈ V ↔ {𝐴} = ∅)
98biimpi 206 . . 3 𝐴 ∈ V → {𝐴} = ∅)
10 0ex 4781 . . 3 ∅ ∈ V
119, 10syl6eqel 2707 . 2 𝐴 ∈ V → {𝐴} ∈ V)
127, 11pm2.61i 176 1 {𝐴} ∈ V
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1481  wcel 1988  Vcvv 3195  c0 3907  {csn 4168  {cpr 4170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-nul 3908  df-sn 4169  df-pr 4171
This theorem is referenced by:  prex  4900  elALT  4901  dtruALT2  4902  snelpwi  4903  snelpw  4904  rext  4907  sspwb  4908  intid  4917  moabex  4918  nnullss  4921  exss  4922  elopg  4925  opi1  4928  op1stb  4931  opnz  4932  opeqsn  4957  opeqpr  4958  propssopi  4961  opthwiener  4966  uniop  4967  frirr  5081  frsn  5179  xpsspw  5223  relop  5261  onnev  5836  funopg  5910  funsneqopsn  6402  funsneqop  6403  fsnex  6523  tpex  6942  snnex  6951  snnexOLD  6952  difsnexi  6955  sucexb  6994  soex  7094  elxp4  7095  elxp5  7096  opabex3d  7130  opabex3  7131  1stval  7155  2ndval  7156  fo1st  7173  fo2nd  7174  mpt2exxg  7229  cnvf1o  7261  fnse  7279  suppsnop  7294  brtpos2  7343  wfrlem15  7414  tfrlem12  7470  tfrlem16  7474  mapsn  7884  fvdiagfn  7887  mapsnconst  7888  mapsncnv  7889  mapsnf1o2  7890  ralxpmap  7892  elixpsn  7932  ixpsnf1o  7933  mapsnf1o  7934  ensn1  8005  en1b  8009  mapsnen  8020  xpsnen  8029  endisj  8032  xpsnen2g  8038  domunsncan  8045  enfixsn  8054  domunsn  8095  fodomr  8096  disjenex  8103  domssex2  8105  domssex  8106  map2xp  8115  phplem2  8125  isinf  8158  pssnn  8163  findcard2  8185  ac6sfi  8189  xpfi  8216  fodomfi  8224  pwfilem  8245  fczfsuppd  8278  snopfsupp  8283  fisn  8318  marypha1lem  8324  brwdom2  8463  unxpwdom2  8478  elirrv  8489  epfrs  8592  tc2  8603  tcsni  8604  ranksuc  8713  fseqenlem1  8832  dfac5lem2  8932  dfac5lem3  8933  dfac5lem4  8934  kmlem2  8958  cdafn  8976  cdaval  8977  cdaassen  8989  mapcdaen  8991  cdadom1  8993  cdainf  8999  ackbij1lem5  9031  cfsuc  9064  isfin1-3  9193  hsmexlem4  9236  axcc2lem  9243  dcomex  9254  axdc3lem4  9260  axdc4lem  9262  ttukeylem3  9318  brdom7disj  9338  brdom6disj  9339  fpwwe2lem13  9449  canthwe  9458  canthp1lem1  9459  uniwun  9547  rankcf  9584  nn0ex  11283  hashxplem  13203  hashmap  13205  hashbclem  13219  hashf1lem1  13222  hashge3el3dif  13251  ofs1  13690  climconst2  14260  incexclem  14549  ramub1lem2  15712  cshwsex  15788  setsvalg  15868  setsid  15895  pwsbas  16128  pwsle  16133  pwssca  16137  pwssnf1o  16139  imasplusg  16158  imasmulr  16159  imasvsca  16161  imasip  16162  xpsc  16198  acsfn  16301  isfunc  16505  homaf  16661  homaval  16662  funcsetcestrclem1  16775  mgm1  17238  sgrp1  17274  mnd1  17312  mnd1id  17313  grp1  17503  grp1inv  17504  symg2bas  17799  idrespermg  17812  pmtrsn  17920  psgnsn  17921  abl1  18250  gsum2d2  18354  gsumcom2  18355  dprdz  18410  dprdsn  18416  dprd2da  18422  ring1  18583  pwssplit3  19042  drngnidl  19210  drnglpir  19234  rng1nnzr  19255  evlssca  19503  mpfind  19517  evls1sca  19669  pf1ind  19700  frlmip  20098  islindf4  20158  mattposvs  20242  mat1dimelbas  20258  mat1dimscm  20262  mat1dimmul  20263  mat1rhmval  20266  m1detdiag  20384  mdetrlin  20389  mdetrsca2  20391  mdetrlin2  20394  mdetunilem5  20403  smadiadetglem2  20459  basdif0  20738  ordtbas  20977  leordtval2  20997  dishaus  21167  discmp  21182  conncompid  21215  dis2ndc  21244  dislly  21281  dis1stc  21283  unisngl  21311  1stckgen  21338  ptbasfi  21365  dfac14lem  21401  dfac14  21402  ptrescn  21423  xkoptsub  21438  pt1hmeo  21590  xpstopnlem1  21593  ptcmpfi  21597  isufil2  21693  ufileu  21704  filufint  21705  uffix  21706  uffixsn  21710  flimclslem  21769  ptcmplem1  21837  cnextfval  21847  imasdsf1olem  22159  icccmplem1  22606  icccmplem2  22607  rrxip  23159  elply2  23933  plyss  23936  plyeq0lem  23947  taylfval  24094  axlowdimlem15  25817  axlowdim  25822  snstriedgval  25911  vtxvalsnop  25914  iedgvalsnop  25915  upgr1eop  25991  upgr1eopALT  25993  uspgr1eop  26120  usgr1eop  26123  lfuhgr1v0e  26127  1loopgrvd2  26380  1loopgrvd0  26381  p1evtxdeqlem  26389  p1evtxdeq  26390  p1evtxdp1  26391  uspgrloopvtx  26392  uspgrloopiedg  26394  uspgrloopedg  26395  wlkp1lem4  26554  0pthonv  26970  eupth2lem3  27076  0ofval  27612  resf1o  29479  ordtconnlem1  29944  esumpr  30102  esumrnmpt2  30104  esumfzf  30105  esum2dlem  30128  esum2d  30129  esumiun  30130  prsiga  30168  rossros  30217  cntnevol  30265  carsgclctunlem1  30353  omsmeas  30359  eulerpartlemgs2  30416  ccatmulgnn0dir  30593  ofcs1  30595  actfunsnf1o  30656  actfunsnrndisj  30657  reprsuc  30667  breprexplema  30682  bnj918  30810  bnj95  30908  bnj1452  31094  bnj1489  31098  subfacp1lem5  31140  erdszelem5  31151  erdszelem8  31154  cvmliftlem4  31244  cvmliftlem5  31245  cvmlift2lem6  31264  cvmlift2lem9  31267  cvmlift2lem12  31270  conway  31884  etasslt  31894  slerec  31897  fobigcup  31982  elsingles  32000  fnsingle  32001  fvsingle  32002  dfiota3  32005  brapply  32020  brsuccf  32023  funpartlem  32024  altopthsn  32043  altxpsspw  32059  hfsn  32261  neibastop2lem  32330  topjoin  32335  onpsstopbas  32404  bj-sels  32925  bj-snsetex  32926  bj-elsngl  32931  bj-2uplex  32985  bj-restsn  33010  bj-snmoore  33043  f1omptsnlem  33154  mptsnunlem  33156  topdifinffinlem  33166  finixpnum  33365  ptrest  33379  poimirlem3  33383  poimirlem4  33384  poimirlem28  33408  fdc  33512  heiborlem3  33583  heiborlem8  33588  ismrer1  33608  grposnOLD  33652  zrdivrng  33723  ldualset  34231  lineset  34843  ispointN  34847  dvaset  36112  dvhset  36189  dibval  36250  dibfna  36262  elrfi  37076  mzpincl  37116  mzpcompact2lem  37133  wopprc  37416  dfac11  37451  kelac2  37454  pwslnmlem1  37481  pwslnm  37483  fvilbdRP  37801  brtrclfv2  37838  frege110  38087  frege133  38110  k0004lem3  38267  snelpwrVD  38886  fnchoice  39008  mapsnd  39204  mapsnend  39207  mpct  39209  elmapsnd  39212  difmapsn  39220  unirnmapsn  39222  ssmapsn  39224  limcresiooub  39674  limcresioolb  39675  cnfdmsn  39858  dvsinax  39890  fourierdlem48  40134  fourierdlem49  40135  salexct3  40323  salgencntex  40324  salgensscntex  40325  sge0sn  40359  sge0p1  40394  sge0xp  40409  ovnovollem1  40633  ovnovollem2  40634  vonvolmbllem  40637  setsv  41112  nnsum3primesprm  41443  mpt2exxg2  41881  mapsnop  41888  lindsrng01  42022  snlindsntorlem  42024  snlindsntor  42025  lmod1lem1  42041  lmod1lem2  42042  lmod1lem3  42043  lmod1lem4  42044  lmod1lem5  42045  lmod1  42046  lmod1zr  42047  aacllem  42312
  Copyright terms: Public domain W3C validator