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

Theorem snid 4402
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
snid.1 𝐴 ∈ V
Assertion
Ref Expression
snid 𝐴 ∈ {𝐴}

Proof of Theorem snid
StepHypRef Expression
1 snid.1 . 2 𝐴 ∈ V
2 snidb 4401 . 2 (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
31, 2mpbi 221 1 𝐴 ∈ {𝐴}
Colors of variables: wff setvar class
Syntax hints:  wcel 2156  Vcvv 3391  {csn 4370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-sn 4371
This theorem is referenced by:  vsnid  4403  rabsnt  4457  sseliALT  4986  elALT  5100  intid  5116  0sn0ep  5228  opthprc  5367  dmsnsnsn  5825  snsn0non  6055  fvrn0  6432  fsn  6621  fsn2  6622  fnsnb  6653  fmptsng  6655  fmptsnd  6656  fvsn  6667  fvsnun1  6669  ovima0  7039  brtpos0  7590  tfrlem11  7716  mapsnd  8130  mapsncnv  8137  0elixp  8172  domunsncan  8295  enfixsn  8304  infeq5i  8776  tc2  8861  djulcl  9015  djurcl  9016  djulf1o  9017  djuun  9031  isfin4-3  9418  fin1a2lem12  9514  dcomex  9550  axdc3lem4  9556  zornn0g  9608  axpowndlem3  9702  canthp1lem2  9756  elreal2  10234  xrinfmss  12354  fseq1p1m1  12633  1exp  13108  wrdexb  13523  divalgmod  15345  0bits  15376  lcmfunsnlem2  15568  0ram  15937  setsid  16121  imasvscafn  16398  imasvscaval  16399  xpsc0  16421  xpsc1  16422  gsumval2  17481  gsumz  17575  psgnsn  18137  psgnprfval2  18140  mat0dimscm  20483  mat0scmat  20552  mvmumamul1  20568  m1detdiag  20611  pmatcoe1fsupp  20716  d0mat2pmat  20753  pmatcollpw3fi1lem1  20801  pmatcollpw3fi1lem2  20802  chpmat0d  20849  dfac14  21632  filconn  21897  uffix  21935  cnextfvval  22079  cnextcn  22081  ust0  22233  bndth  22967  minveclem4a  23412  dvef  23956  tdeglem2  24034  mdegcl  24042  aalioulem2  24301  cxplogb  24737  xrlimcnp  24908  gausslemma2dlem4  25307  axlowdimlem8  26042  axlowdimlem11  26045  upgr1e  26221  uspgr1e  26351  wlkl1loop  26761  wlk1walk  26762  wlk2v2elem1  27327  frgrncvvdeqlem7  27479  hsn0elch  28432  rabsnel  29665  aciunf1lem  29788  signstfvn  30970  repr0  31013  bnj97  31257  bnj553  31289  bnj966  31335  bnj1442  31438  subfacp1lem2a  31483  subfacp1lem5  31487  cvmliftlem4  31591  bj-0eltag  33274  cnfin0  33554  poimirlem3  33723  poimirlem9  33729  poimirlem31  33751  poimirlem32  33752  prdsbnd  33901  heiborlem3  33921  grposnOLD  33990  grpokerinj  34001  0idl  34133  0rngo  34135  fvilbdRP  38479  frege54cor1c  38706  binomcxplemnotnn0  39052  snsslVD  39555  snssl  39556  unipwrVD  39558  unipwr  39559  sucidALTVD  39597  sucidALT  39598  sucidVD  39599  unisnALT  39653  eliuniincex  39781  cnrefiisplem  40532  0cnf  40567  dvmptfprod  40637  qndenserrnbl  40991  nnfoctbdjlem  41148  isomenndlem  41223  hoidmvlelem2  41289  hoiqssbl  41318  funressnfv  41659  el1fzopredsuc  41907  setsidel  41918  sbgoldbo  42247  c0snmhm  42480  lincval0  42769  lcoel0  42782
  Copyright terms: Public domain W3C validator