Theorem snssi 4807

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 4782	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
2	1	ibi 266	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2099   ⊆ wss 3946  {csn 4623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-ss 3963  df-sn 4624

This theorem is referenced by:  snssd  4808  difsnid  4809  eldifeldifsn  4810  pwpw0  4812  sssn  4825  ssunsn2  4826  tpssi  4837  snelpwiOLD  5440  intidOLD  5454  frirr  5649  xpsspw  5805  djussxp  5842  dmressnsn  6022  fconst6g  6780  f1sng  6874  dffv2  6986  fvimacnvi  7054  fvimacnvALT  7059  fsn2  7139  fsnunf  7188  abnexg  7753  ordsuci  7806  sucexeloniOLD  7808  suceloniOLD  7810  curry1  8107  curry2  8110  xpord2pred  8148  xpord3pred  8155  ressuppss  8186  ressuppssdif  8188  naddcllem  8695  naddov2  8698  mapsnd  8904  ralxpmap  8914  sucdom2OLD  9109  fodomr  9155  findcard2  9191  findcard2s  9192  unfi  9199  ssfi  9201  sucdom2  9230  0sdom1dom  9262  en1eqsnOLD  9299  enp1ilem  9302  findcard2OLD  9308  fodomfir  9360  marypha1lem  9466  marypha2lem1  9468  epfrs  9764  dfac5lem4  10159  kmlem11  10193  ackbij1lem2  10252  fin23lem26  10356  isfin1-3  10417  hsmexlem4  10460  axdc3lem4  10484  axresscn  11179  nn0ssre  12519  nn0sscn  12520  xrsupss  13333  supxrmnf  13341  1exp  14102  hashxrcl  14366  hashdifsn  14423  hashdifsnp1  14507  repsdf2  14778  modfsummods  15789  fsum00  15794  incexc  15833  2ebits  16439  bitsinvp1  16441  lcmfunsnlem2lem1  16631  lcmfunsnlem2lem2  16632  lcmfunsnlem2  16633  coprmproddvdslem  16655  4sqlem19  16957  ramxrcl  17011  mrcsncl  17617  acsfn1  17666  homaf  18044  dmcoass  18080  lubel  18531  gsumws1  18820  eqg0subgecsn  19184  cycsubg2  19197  cntzsnval  19311  0frgp  19770  dpjidcl  20051  ablfac1eu  20066  lspsncl  20947  lspsnss  20960  lspsnid  20963  lpival  21306  lpiss  21311  lidldvgen  21316  pzriprnglem10  21473  znlidl  21520  frlmlbs  21788  mat1dimelbas  22458  smadiadetglem2  22659  isneip  23094  neips  23102  opnneip  23108  maxlp  23136  restsn2  23160  leordtval2  23201  ist1-3  23338  ordtt1  23368  2ndcdisj2  23446  uffix  23910  neiflim  23963  ptcmplem5  24045  cnextfres1  24057  haustsms2  24126  ust0  24209  ustuqtop5  24235  dscopn  24567  icccmplem1  24823  bndth  24969  ovolsn  25509  icombl1  25577  plyun0  26218  coeeulem  26245  coeeu  26246  vieta1lem2  26333  aalioulem2  26355  taylfval  26380  perfectlem2  27253  noextend  27690  noextendseq  27691  conway  27823  etasslt  27837  0slt1s  27853  ssltleft  27888  ssltright  27889  negsid  28044  precsexlem8  28207  precsexlem11  28210  n0sbday  28314  istrkg2ld  28381  axlowdimlem7  28876  axlowdimlem10  28879  0clwlkv  30058  hsn0elch  31175  chsupsn  31340  chsup0  31475  h1deoi  31476  h1dei  31477  h1did  31478  h1de2ctlem  31482  h1de2ci  31483  spansni  31484  spansnch  31487  elspansncl  31492  spansnpji  31505  spanunsni  31506  spanpr  31507  h1datomi  31508  spansnji  31573  h1da  32276  atom1d  32280  superpos  32281  disjun0  32512  djussxp2  32562  mptprop  32607  pwrssmgc  32870  1fldgenq  33174  rspsnid  33249  lindssn  33256  elrspunidl  33306  lbslsat  33514  esumnul  33891  esumcst  33906  hashf2  33927  esum2d  33936  measvuni  34057  cntnevol  34071  eulerpartlemt  34215  eulerpartlemmf  34219  eulerpartlemgh  34222  ballotlemfp1  34335  reprinfz1  34478  fineqvac  34943  f1resfz0f1d  34951  dfon2lem3  35619  altxpsspw  35811  bj-snglss  36687  lindsadd  37324  lindsenlbs  37326  poimirlem16  37347  poimirlem19  37350  poimirlem23  37354  poimirlem25  37356  poimirlem29  37360  poimirlem31  37362  mblfinlem2  37369  dvasin  37415  fdc  37456  prnc  37778  isfldidl  37779  ispridlc  37781  islshpsm  38688  snatpsubN  39459  polatN  39640  atpsubclN  39654  pclfinclN  39659  mapfzcons  42407  mzpcompact2lem  42442  diophrw  42450  brfvidRP  43389  cotrcltrcl  43426  corcltrcl  43440  cotrclrcl  43443  gneispa  43831  binomcxplemnotnn0  44064  snelpwrVD  44541  disjiun2  44693  infxrpnf  45094  mccllem  45251  islptre  45273  cncfdmsn  45544  snmbl  45617  stoweidlem44  45698  sge0tsms  46034  sge0iunmptlemfi  46067  ismeannd  46121  isomenndlem  46184  hoidmvlelem3  46251  hoidmvlelem4  46252  ovnhoilem1  46255  fnbrafvb  46800  afvres  46818  afv2res  46885  perfectALTVlem2  47327  mapsnop  47756  lincext2  47871  snlindsntorlem  47886  aacllem  48582