Theorem snssi 4701

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

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  {csn 4525

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-sn 4526

This theorem is referenced by:  snssd  4702  difsnid  4703  eldifeldifsn  4704  pwpw0  4706  sssn  4719  ssunsn2  4720  tpssi  4729  pwsnOLD  4793  snelpwi  5302  intid  5315  frirr  5496  xpsspw  5646  djussxp  5680  dmressnsn  5860  fconst6g  6542  f1sng  6631  dffv2  6733  fvimacnvi  6799  fvimacnvALT  6804  fsn2  6875  fsnunf  6924  abnexg  7458  suceloni  7508  curry1  7782  curry2  7785  ressuppss  7832  ressuppssdif  7834  mapsnd  8433  ralxpmap  8443  sucdom2  8610  fodomr  8652  en1eqsn  8732  enp1ilem  8736  findcard2  8742  findcard2s  8743  marypha1lem  8881  marypha2lem1  8883  epfrs  9157  dfac5lem4  9537  kmlem11  9571  ackbij1lem2  9632  fin23lem26  9736  isfin1-3  9797  hsmexlem4  9840  axdc3lem4  9864  axresscn  10559  nn0ssre  11889  nn0sscn  11890  xrsupss  12690  supxrmnf  12698  1exp  13454  hashxrcl  13714  hashdifsn  13771  hashdifsnp1  13850  repsdf2  14131  modfsummods  15140  fsum00  15145  incexc  15184  2ebits  15786  bitsinvp1  15788  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  coprmproddvdslem  15996  4sqlem19  16289  ramxrcl  16343  mrcsncl  16875  acsfn1  16924  homaf  17282  dmcoass  17318  lubel  17724  gsumws1  17994  cycsubg2  18345  cntzsnval  18446  0frgp  18897  dpjidcl  19173  ablfac1eu  19188  lspsncl  19742  lspsnss  19755  lspsnid  19758  lpival  20011  lpiss  20016  lidldvgen  20021  znlidl  20225  frlmlbs  20486  mat1dimelbas  21076  smadiadetglem2  21277  isneip  21710  neips  21718  opnneip  21724  maxlp  21752  restsn2  21776  leordtval2  21817  ist1-3  21954  ordtt1  21984  2ndcdisj2  22062  uffix  22526  neiflim  22579  ptcmplem5  22661  cnextfres1  22673  haustsms2  22742  ust0  22825  ustuqtop5  22851  dscopn  23180  icccmplem1  23427  bndth  23563  ovolsn  24099  icombl1  24167  plyun0  24794  coeeulem  24821  coeeu  24822  vieta1lem2  24907  aalioulem2  24929  taylfval  24954  perfectlem2  25814  istrkg2ld  26254  axlowdimlem7  26742  axlowdimlem10  26745  0clwlkv  27916  hsn0elch  29031  chsupsn  29196  chsup0  29331  h1deoi  29332  h1dei  29333  h1did  29334  h1de2ctlem  29338  h1de2ci  29339  spansni  29340  spansnch  29343  elspansncl  29348  spansnpji  29361  spanunsni  29362  spanpr  29363  h1datomi  29364  spansnji  29429  h1da  30132  atom1d  30136  superpos  30137  disjun0  30358  djussxp2  30410  mptprop  30458  pwrssmgc  30706  rspsnid  30988  lindssn  30993  elrspunidl  31014  lbslsat  31102  esumnul  31417  esumcst  31432  hashf2  31453  esum2d  31462  measvuni  31583  cntnevol  31597  eulerpartlemt  31739  eulerpartlemmf  31743  eulerpartlemgh  31746  ballotlemfp1  31859  reprinfz1  32003  f1resfz0f1d  32471  dfon2lem3  33143  noextend  33286  noextendseq  33287  conway  33377  etasslt  33387  altxpsspw  33551  bj-snglss  34406  lindsadd  35050  lindsenlbs  35052  poimirlem16  35073  poimirlem19  35076  poimirlem23  35080  poimirlem25  35082  poimirlem29  35086  poimirlem31  35088  mblfinlem2  35095  dvasin  35141  fdc  35183  prnc  35505  isfldidl  35506  ispridlc  35508  islshpsm  36276  snatpsubN  37046  polatN  37227  atpsubclN  37241  pclfinclN  37246  mapfzcons  39657  mzpcompact2lem  39692  diophrw  39700  brfvidRP  40389  cotrcltrcl  40426  corcltrcl  40440  cotrclrcl  40443  gneispa  40833  binomcxplemnotnn0  41060  snelpwrVD  41537  disjiun2  41692  infxrpnf  42084  mccllem  42239  islptre  42261  cncfdmsn  42532  snmbl  42605  stoweidlem44  42686  sge0tsms  43019  sge0iunmptlemfi  43052  ismeannd  43106  isomenndlem  43169  hoidmvlelem3  43236  hoidmvlelem4  43237  ovnhoilem1  43240  fnbrafvb  43710  afvres  43728  afv2res  43795  perfectALTVlem2  44240  mapsnop  44746  lincext2  44864  snlindsntorlem  44879  aacllem  45329