Theorem snssi 4101

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	|- ( A e. B -> { A } C_ B )

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 4090	. 2 |- ( A e. B -> ( A e. B <-> { A } C_ B ) )
2	1	ibi 241	1 |- ( A e. B -> { A } C_ B )

Syntax hints:   -> wi 4   e. wcel 1836   C_ wss 3402   {csn 3957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-clab 2378  df-cleq 2384  df-clel 2387  df-v 3049  df-in 3409  df-ss 3416  df-sn 3958

This theorem is referenced by:  difsnid  4103  pwpw0  4105  sssn  4115  ssunsn2  4116  tpssi  4123  pwsnALT  4171  snelpwi  4620  intid  4633  xpsspw  5042  djussxp  5074  dmressnsn  5237  fconst6g  5695  dffv2  5860  fvimacnvi  5916  fvimacnvALT  5921  fsn2  5985  fsnunf  6025  suceloni  6565  curry1  6809  curry2  6812  ressuppss  6855  ressuppssdif  6857  mapsn  7397  ralxpmap  7405  fodomr  7605  sucdom2  7650  en1eqsn  7683  enp1ilem  7687  findcard2  7693  findcard2s  7694  marypha1lem  7826  marypha2lem1  7828  epfrs  8093  dfac5lem4  8438  kmlem11  8471  ackbij1lem2  8532  fin23lem26  8636  isfin1-3  8697  hsmexlem4  8740  axdc3lem4  8764  axresscn  9454  nn0ssre  10734  xrsupss  11439  supxrmnf  11448  1fv  11732  1exp  12117  hashxrcl  12350  hashdifsn  12400  brfi1indlem  12454  snopiswrd  12482  repsdf2  12680  modfsummods  13628  fsum00  13633  incexc  13670  2ebits  14118  bitsinvp1  14120  4sqlem19  14502  ramxrcl  14556  strlemor1  14748  mrcsncl  15038  acsfn1  15087  homaf  15445  dmcoass  15481  lubel  15888  gsumws1  16143  cycsubg2  16374  cntzsnval  16498  0frgp  16933  dpjidcl  17239  dpjidclOLD  17246  ablfac1eu  17256  lspsncl  17755  lspsnss  17768  lspsnid  17771  lpival  18025  lpiss  18030  lidldvgen  18035  znlidl  18682  frgpcyg  18722  frlmlbs  18936  mat1dimelbas  19077  mat1dimmul  19082  smadiadetglem2  19278  isneip  19711  neips  19719  opnneip  19725  maxlp  19753  restsn2  19777  leordtval2  19818  ist1-3  19955  ordtt1  19985  2ndcdisj2  20062  uffix  20526  neiflim  20579  ptcmplem5  20660  cnextfres  20672  haustsms2  20739  ust0  20826  ustuqtop5  20852  dscopn  21198  icccmplem1  21431  bndth  21562  ovolsn  22010  icombl1  22077  plyun0  22698  coeeulem  22725  coeeu  22726  vieta1lem2  22811  aalioulem2  22833  taylfval  22858  perfectlem2  23641  istrkg2ld  23994  axlowdimlem7  24393  axlowdimlem10  24396  konigsberg  25129  hsn0elch  26304  chsupsn  26469  chsup0  26604  h1deoi  26605  h1dei  26606  h1did  26607  h1de2ctlem  26611  h1de2ci  26612  spansni  26613  spansnch  26616  elspansncl  26621  spansnpji  26634  spanunsni  26635  spanpr  26636  h1datomi  26637  spansnji  26702  h1da  27405  atom1d  27409  superpos  27410  disjun0  27614  esumnul  28227  esumcst  28242  hashf2  28263  esum2d  28272  measvuni  28377  cntnevol  28391  eulerpartlemt  28529  eulerpartlemmf  28533  eulerpartlemgh  28536  ballotlemfp1  28649  dfon2lem3  29418  altxpsspw  29816  mblfinlem2  30253  dvasin  30305  fdc  30440  prnc  30666  isfldidl  30667  ispridlc  30669  mapfzcons  30850  mzpcompact2lem  30885  diophrw  30893  binomcxplemnotnn0  31465  fprodsplit1f  31794  mccllem  31806  islptre  31826  cncfdmsn  31894  snmbl  31963  stoweidlem44  32027  fnbrafvb  32440  afvres  32458  perfectALTVlem2  32579  mapsnop  33169  lincext2  33291  snlindsntorlem  33306  aacllem  33585  snelpwrVD  34012  bj-snglss  34911  islshpsm  35153  snatpsubN  35922  polatN  36103  atpsubclN  36117  pclfinclN  36122  corcltrcl  38284  cotrclrcl  38285  cotrcltrcl  38286