Theorem snssi 4766

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-sn 4583

This theorem is referenced by:  snssd  4767  difsnid  4768  eldifeldifsn  4769  pwpw0  4771  sssn  4784  ssunsn2  4785  tpssi  4796  frirr  5608  xpsspw  5766  djussxp  5802  dmressnsn  5990  fconst6g  6731  f1sng  6825  dffv2  6937  fvimacnvi  7006  fvimacnvALT  7011  fsn2  7091  fsnunf  7141  abnexg  7711  ordsuci  7763  curry1  8056  curry2  8059  xpord2pred  8097  xpord3pred  8104  ressuppss  8135  ressuppssdif  8137  naddcllem  8614  naddov2  8617  mapsnd  8836  ralxpmap  8846  fodomr  9068  findcard2  9101  findcard2s  9102  unfi  9107  ssfi  9109  sucdom2  9139  0sdom1dom  9158  enp1ilem  9190  fodomfir  9240  marypha1lem  9348  marypha2lem1  9350  epfrs  9652  dfac5lem4  10048  dfac5lem4OLD  10050  kmlem11  10083  ackbij1lem2  10142  fin23lem26  10247  isfin1-3  10308  hsmexlem4  10351  axdc3lem4  10375  axresscn  11071  nn0ssre  12417  nn0sscn  12418  xrsupss  13236  supxrmnf  13244  1exp  14026  hashxrcl  14292  hashdifsn  14349  hashdifsnp1  14441  repsdf2  14713  modfsummods  15728  fsum00  15733  incexc  15772  2ebits  16386  bitsinvp1  16388  lcmfunsnlem2lem1  16577  lcmfunsnlem2lem2  16578  lcmfunsnlem2  16579  coprmproddvdslem  16601  4sqlem19  16903  ramxrcl  16957  mrcsncl  17547  acsfn1  17596  homaf  17966  dmcoass  18002  lubel  18449  gsumws1  18775  eqg0subgecsn  19138  cycsubg2  19151  cntzsnval  19265  0frgp  19720  dpjidcl  20001  ablfac1eu  20016  lspsncl  20940  lspsnss  20953  lspsnid  20956  lpival  21291  lpiss  21296  lidldvgen  21301  pzriprnglem10  21457  znlidl  21500  frlmlbs  21764  mat1dimelbas  22427  smadiadetglem2  22628  isneip  23061  neips  23069  opnneip  23075  maxlp  23103  restsn2  23127  leordtval2  23168  ist1-3  23305  ordtt1  23335  2ndcdisj2  23413  uffix  23877  neiflim  23930  ptcmplem5  24012  cnextfres1  24024  haustsms2  24093  ust0  24176  ustuqtop5  24201  dscopn  24529  icccmplem1  24779  bndth  24925  ovolsn  25464  icombl1  25532  plyun0  26170  coeeulem  26197  coeeu  26198  vieta1lem2  26287  aalioulem2  26309  taylfval  26334  perfectlem2  27209  noextend  27646  noextendseq  27647  conway  27787  etaslts  27801  0lt1s  27820  sltsleft  27868  sltsright  27869  negsid  28049  precsexlem8  28222  precsexlem11  28225  n0bday  28360  elreno2  28503  istrkg2ld  28544  axlowdimlem7  29033  axlowdimlem10  29036  0clwlkv  30218  hsn0elch  31336  chsupsn  31501  chsup0  31636  h1deoi  31637  h1dei  31638  h1did  31639  h1de2ctlem  31643  h1de2ci  31644  spansni  31645  spansnch  31648  elspansncl  31653  spansnpji  31666  spanunsni  31667  spanpr  31668  h1datomi  31669  spansnji  31734  h1da  32437  atom1d  32441  superpos  32442  disjun0  32682  djussxp2  32738  mptprop  32788  pwrssmgc  33093  gsumwrd2dccatlem  33171  elrgspnsubrunlem2  33342  1fldgenq  33416  rspsnid  33464  lindssn  33471  elrspunidl  33521  esplyfval1  33750  esplyfvaln  33751  lbslsat  33794  fldextrspunlsplem  33851  esumnul  34226  esumcst  34241  hashf2  34262  esum2d  34271  measvuni  34392  cntnevol  34406  eulerpartlemt  34549  eulerpartlemmf  34553  eulerpartlemgh  34556  ballotlemfp1  34670  reprinfz1  34800  fineqvac  35294  f1resfz0f1d  35330  dfon2lem3  35999  altxpsspw  36193  bj-snglss  37218  lindsadd  37864  lindsenlbs  37866  poimirlem16  37887  poimirlem19  37890  poimirlem23  37894  poimirlem25  37896  poimirlem29  37900  poimirlem31  37902  mblfinlem2  37909  dvasin  37955  fdc  37996  prnc  38318  isfldidl  38319  ispridlc  38321  islshpsm  39356  snatpsubN  40126  polatN  40307  atpsubclN  40321  pclfinclN  40326  readvrec2  42731  mapfzcons  43073  mzpcompact2lem  43108  diophrw  43116  brfvidRP  44044  cotrcltrcl  44081  corcltrcl  44095  cotrclrcl  44098  gneispa  44486  binomcxplemnotnn0  44712  snelpwrVD  45186  disjiun2  45418  infxrpnf  45804  mccllem  45957  islptre  45979  cncfdmsn  46248  snmbl  46321  stoweidlem44  46402  sge0tsms  46738  sge0iunmptlemfi  46771  ismeannd  46825  isomenndlem  46888  hoidmvlelem3  46955  hoidmvlelem4  46956  ovnhoilem1  46959  fnbrafvb  47514  afvres  47532  afv2res  47599  perfectALTVlem2  48082  mapsnop  48704  lincext2  48815  snlindsntorlem  48830  resinsnALT  49232  aacllem  50160