Theorem snssi 3902

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 3892	. 2 |- ( A e. B -> ( A e. B <-> { A } C_ B ) )
2	1	ibi 233	1 |- ( A e. B -> { A } C_ B )

Syntax hints:   -> wi 4   e. wcel 1721   C_ wss 3280   {csn 3774

This theorem is referenced by:  difsnid  3904  pwpw0  3906  sssn  3917  ssunsn2  3918  tpssi  3925  pwsnALT  3970  snelpwi  4369  intid  4381  suceloni  4752  xpsspw  4945  xpsspwOLD  4946  djussxp  4977  xpimasn  5275  fconst6g  5591  dffv2  5755  fvimacnvi  5803  fvimacnvALT  5808  fsn2  5867  fsnunf  5890  curry1  6397  curry2  6400  mapsn  7014  fodomr  7217  sucdom2  7262  en1eqsn  7297  enp1ilem  7301  findcard2  7307  findcard2s  7308  marypha1lem  7396  marypha2lem1  7398  epfrs  7623  dfac5lem4  7963  kmlem11  7996  ackbij1lem2  8057  fin23lem26  8161  isfin1-3  8222  hsmexlem4  8265  axdc3lem4  8289  axresscn  8979  nn0ssre  10181  xrsupss  10843  supxrmnf  10852  1fv  11075  1exp  11364  hashxrcl  11595  hashdifsn  11634  brfi1indlem  11669  s1cl  11710  fsum00  12532  incexc  12572  xpnnenOLD  12764  2ebits  12914  bitsinvp1  12916  4sqlem19  13286  ramxrcl  13340  strlemor1  13511  mrcsncl  13792  acsfn1  13841  homaf  14140  dmcoass  14176  lubel  14504  gsumws1  14740  cycsubg2  14932  cntzsnval  15078  0frgp  15366  dpjidcl  15571  ablfac1eu  15586  lspsncl  16008  lspsnss  16021  lspsnid  16024  lpival  16271  lpiss  16276  lidldvgen  16281  znlidl  16769  frgpcyg  16809  isneip  17124  neips  17132  opnneip  17138  maxlp  17165  restsn2  17189  leordtval2  17230  ist1-3  17367  ordtt1  17397  2ndcdisj2  17473  uffix  17906  neiflim  17959  ptcmplem5  18040  cnextfres  18052  haustsms2  18119  ust0  18202  ustuqtop5  18228  dscopn  18574  icccmplem1  18806  bndth  18936  ovolsn  19344  icombl1  19410  plyun0  20069  coeeulem  20096  coeeu  20097  vieta1lem2  20181  aalioulem2  20203  taylfval  20228  perfectlem2  20967  konigsberg  21662  hsn0elch  22703  chsupsn  22868  chsup0  23003  h1deoi  23004  h1dei  23005  h1did  23006  h1de2ctlem  23010  h1de2ci  23011  spansni  23012  spansnch  23015  elspansncl  23020  spansnpji  23033  spanunsni  23034  spanpr  23035  h1datomi  23036  spansnji  23101  h1da  23805  atom1d  23809  superpos  23810  esumnul  24396  esumcst  24408  hashf2  24427  measvuni  24521  cntnevol  24535  ballotlemfp1  24702  dfon2lem3  25355  altxpsspw  25726  axlowdimlem7  25791  axlowdimlem10  25794  mblfinlem  26143  dvreasin  26179  fdc  26339  prnc  26567  isfldidl  26568  ispridlc  26570  ralxpmap  26632  mapfzcons  26662  mzpcompact2lem  26698  diophrw  26707  frlmlbs  27117  stoweidlem44  27660  dmressnsn  27852  fnbrafvb  27885  afvres  27903  snelpwrVD  28652  islshpsm  29463  snatpsubN  30232  polatN  30413  atpsubclN  30427  pclfinclN  30432

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294  df-sn 3780