Theorem snssi 4747

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

Syntax hints:   → wi 4   ∈ wcel 2110   ⊆ wss 3892  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909  df-sn 4568

This theorem is referenced by:  snssd  4748  difsnid  4749  eldifeldifsn  4750  pwpw0  4752  sssn  4765  ssunsn2  4766  tpssi  4775  pwsnOLD  4838  snelpwi  5364  intid  5377  frirr  5567  xpsspw  5718  djussxp  5753  dmressnsn  5932  fconst6g  6661  f1sng  6755  dffv2  6860  fvimacnvi  6926  fvimacnvALT  6931  fsn2  7005  fsnunf  7054  abnexg  7600  sucexeloni  7652  suceloniOLD  7654  curry1  7935  curry2  7938  ressuppss  7990  ressuppssdif  7992  mapsnd  8657  ralxpmap  8667  sucdom2  8851  fodomr  8897  findcard2  8929  findcard2s  8930  unfi  8937  ssfi  8938  en1eqsn  9026  enp1ilem  9029  findcard2OLD  9034  marypha1lem  9170  marypha2lem1  9172  epfrs  9489  dfac5lem4  9883  kmlem11  9917  ackbij1lem2  9978  fin23lem26  10082  isfin1-3  10143  hsmexlem4  10186  axdc3lem4  10210  axresscn  10905  nn0ssre  12237  nn0sscn  12238  xrsupss  13042  supxrmnf  13050  1exp  13810  hashxrcl  14070  hashdifsn  14127  hashdifsnp1  14208  repsdf2  14489  modfsummods  15503  fsum00  15508  incexc  15547  2ebits  16152  bitsinvp1  16154  lcmfunsnlem2lem1  16341  lcmfunsnlem2lem2  16342  lcmfunsnlem2  16343  coprmproddvdslem  16365  4sqlem19  16662  ramxrcl  16716  mrcsncl  17319  acsfn1  17368  homaf  17743  dmcoass  17779  lubel  18230  gsumws1  18474  cycsubg2  18827  cntzsnval  18928  0frgp  19383  dpjidcl  19659  ablfac1eu  19674  lspsncl  20237  lspsnss  20250  lspsnid  20253  lpival  20514  lpiss  20519  lidldvgen  20524  znlidl  20735  frlmlbs  21002  mat1dimelbas  21618  smadiadetglem2  21819  isneip  22254  neips  22262  opnneip  22268  maxlp  22296  restsn2  22320  leordtval2  22361  ist1-3  22498  ordtt1  22528  2ndcdisj2  22606  uffix  23070  neiflim  23123  ptcmplem5  23205  cnextfres1  23217  haustsms2  23286  ust0  23369  ustuqtop5  23395  dscopn  23727  icccmplem1  23983  bndth  24119  ovolsn  24657  icombl1  24725  plyun0  25356  coeeulem  25383  coeeu  25384  vieta1lem2  25469  aalioulem2  25491  taylfval  25516  perfectlem2  26376  istrkg2ld  26819  axlowdimlem7  27314  axlowdimlem10  27317  0clwlkv  28491  hsn0elch  29606  chsupsn  29771  chsup0  29906  h1deoi  29907  h1dei  29908  h1did  29909  h1de2ctlem  29913  h1de2ci  29914  spansni  29915  spansnch  29918  elspansncl  29923  spansnpji  29936  spanunsni  29937  spanpr  29938  h1datomi  29939  spansnji  30004  h1da  30707  atom1d  30711  superpos  30712  disjun0  30930  djussxp2  30981  mptprop  31027  pwrssmgc  31274  rspsnid  31564  lindssn  31569  elrspunidl  31602  lbslsat  31695  esumnul  32012  esumcst  32027  hashf2  32048  esum2d  32057  measvuni  32178  cntnevol  32192  eulerpartlemt  32334  eulerpartlemmf  32338  eulerpartlemgh  32341  ballotlemfp1  32454  reprinfz1  32598  fineqvac  33062  f1resfz0f1d  33068  dfon2lem3  33757  xpord2pred  33788  xpord3pred  33794  naddcllem  33827  naddov2  33830  noextend  33865  noextendseq  33866  conway  33989  etasslt  34003  0slt1s  34019  ssltleft  34050  ssltright  34051  addscllem1  34127  altxpsspw  34275  bj-snglss  35156  lindsadd  35766  lindsenlbs  35768  poimirlem16  35789  poimirlem19  35792  poimirlem23  35796  poimirlem25  35798  poimirlem29  35802  poimirlem31  35804  mblfinlem2  35811  dvasin  35857  fdc  35899  prnc  36221  isfldidl  36222  ispridlc  36224  islshpsm  36990  snatpsubN  37760  polatN  37941  atpsubclN  37955  pclfinclN  37960  mapfzcons  40535  mzpcompact2lem  40570  diophrw  40578  brfvidRP  41266  cotrcltrcl  41303  corcltrcl  41317  cotrclrcl  41320  gneispa  41710  binomcxplemnotnn0  41944  snelpwrVD  42421  disjiun2  42576  infxrpnf  42957  mccllem  43109  islptre  43131  cncfdmsn  43402  snmbl  43475  stoweidlem44  43556  sge0tsms  43889  sge0iunmptlemfi  43922  ismeannd  43976  isomenndlem  44039  hoidmvlelem3  44106  hoidmvlelem4  44107  ovnhoilem1  44110  fnbrafvb  44614  afvres  44632  afv2res  44699  perfectALTVlem2  45143  mapsnop  45649  lincext2  45765  snlindsntorlem  45780  aacllem  46474