Theorem snssi 4536

Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.)

Assertion

Ref	Expression
snssi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 4512	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 258	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2157   ⊆ wss 3776  {csn 4377

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 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-v 3400  df-in 3783  df-ss 3790  df-sn 4378

This theorem is referenced by:  snssd  4537  difsnid  4538  eldifeldifsn  4539  pwpw0  4541  sssn  4554  ssunsn2  4555  tpssi  4564  pwsnALT  4630  snelpwi  5109  intid  5123  frirr  5295  xpsspw  5441  djussxp  5476  dmressnsn  5650  fconst6g  6312  f1sng  6397  dffv2  6495  fvimacnvi  6556  fvimacnvALT  6561  fsn2  6629  fsnunf  6679  abnexg  7197  suceloni  7246  curry1  7506  curry2  7509  ressuppss  7551  ressuppssdif  7553  mapsnd  8137  ralxpmap  8147  fodomr  8353  sucdom2  8398  en1eqsn  8432  enp1ilem  8436  findcard2  8442  findcard2s  8443  marypha1lem  8581  marypha2lem1  8583  epfrs  8857  dfac5lem4  9235  kmlem11  9270  ackbij1lem2  9331  fin23lem26  9435  isfin1-3  9496  hsmexlem4  9539  axdc3lem4  9563  axresscn  10257  nn0ssre  11566  xrsupss  12360  supxrmnf  12368  1exp  13115  hashxrcl  13369  hashdifsn  13422  hashdifsnp1  13498  repsdf2  13752  modfsummods  14750  fsum00  14755  incexc  14794  fprodsplit1f  14944  2ebits  15391  bitsinvp1  15393  lcmfunsnlem2lem1  15573  lcmfunsnlem2lem2  15574  lcmfunsnlem2  15575  coprmproddvdslem  15597  4sqlem19  15887  ramxrcl  15941  strlemor1OLD  16183  mrcsncl  16480  acsfn1  16529  homaf  16887  dmcoass  16923  lubel  17330  gsumws1  17584  cycsubg2  17836  cntzsnval  17961  0frgp  18396  dpjidcl  18662  ablfac1eu  18677  lspsncl  19187  lspsnss  19200  lspsnid  19203  lpival  19457  lpiss  19462  lidldvgen  19467  znlidl  20092  frlmlbs  20350  mat1dimelbas  20492  smadiadetglem2  20694  isneip  21127  neips  21135  opnneip  21141  maxlp  21169  restsn2  21193  leordtval2  21234  ist1-3  21371  ordtt1  21401  2ndcdisj2  21478  uffix  21942  neiflim  21995  ptcmplem5  22077  cnextfres1  22089  haustsms2  22157  ust0  22240  ustuqtop5  22266  dscopn  22595  icccmplem1  22842  bndth  22974  ovolsn  23482  icombl1  23550  plyun0  24173  coeeulem  24200  coeeu  24201  vieta1lem2  24286  aalioulem2  24308  taylfval  24333  perfectlem2  25175  istrkg2ld  25579  axlowdimlem7  26048  axlowdimlem10  26051  0clwlkv  27310  hsn0elch  28439  chsupsn  28606  chsup0  28741  h1deoi  28742  h1dei  28743  h1did  28744  h1de2ctlem  28748  h1de2ci  28749  spansni  28750  spansnch  28753  elspansncl  28758  spansnpji  28771  spanunsni  28772  spanpr  28773  h1datomi  28774  spansnji  28839  h1da  29542  atom1d  29546  superpos  29547  disjun0  29739  esumnul  30441  esumcst  30456  hashf2  30477  esum2d  30486  measvuni  30608  cntnevol  30622  eulerpartlemt  30764  eulerpartlemmf  30768  eulerpartlemgh  30771  ballotlemfp1  30884  reprinfz1  31031  dfon2lem3  32015  noextend  32145  noextendseq  32146  conway  32236  etasslt  32246  altxpsspw  32410  bj-snglss  33270  lindsenlbs  33719  poimirlem16  33740  poimirlem19  33743  poimirlem23  33747  poimirlem25  33749  poimirlem29  33753  poimirlem31  33755  mblfinlem2  33762  dvasin  33810  fdc  33854  prnc  34179  isfldidl  34180  ispridlc  34182  islshpsm  34762  snatpsubN  35532  polatN  35713  atpsubclN  35727  pclfinclN  35732  mapfzcons  37782  mzpcompact2lem  37817  diophrw  37825  brfvidRP  38481  cotrcltrcl  38518  corcltrcl  38532  cotrclrcl  38535  gneispa  38929  binomcxplemnotnn0  39056  snelpwrVD  39561  disjiun2  39720  infxrpnf  40154  mccllem  40310  islptre  40332  cncfdmsn  40584  snmbl  40659  stoweidlem44  40741  sge0tsms  41077  sge0iunmptlemfi  41110  ismeannd  41164  isomenndlem  41227  hoidmvlelem3  41294  hoidmvlelem4  41295  ovnhoilem1  41298  fnbrafvb  41744  afvres  41762  afv2res  41829  perfectALTVlem2  42207  mapsnop  42692  lincext2  42813  snlindsntorlem  42828  aacllem  43119