Theorem snssi 4129

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

Syntax hints:   -> wi 4   e. wcel 1898   C_ wss 3416   {csn 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-v 3059  df-in 3423  df-ss 3430  df-sn 3981

This theorem is referenced by:  difsnid  4131  pwpw0  4133  sssn  4143  ssunsn2  4144  tpssi  4151  pwsnALT  4207  snelpwi  4659  intid  4672  xpsspw  4967  djussxp  4999  dmressnsn  5162  fconst6g  5795  dffv2  5961  fvimacnvi  6019  fvimacnvALT  6024  fsn2  6086  fsnunf  6126  suceloni  6667  curry1  6915  curry2  6918  ressuppss  6961  ressuppssdif  6963  mapsn  7539  ralxpmap  7547  fodomr  7749  sucdom2  7794  en1eqsn  7827  enp1ilem  7831  findcard2  7837  findcard2s  7838  marypha1lem  7973  marypha2lem1  7975  epfrs  8241  dfac5lem4  8583  kmlem11  8616  ackbij1lem2  8677  fin23lem26  8781  isfin1-3  8842  hsmexlem4  8885  axdc3lem4  8909  axresscn  9598  nn0ssre  10902  xrsupss  11623  supxrmnf  11632  1fv  11939  1exp  12333  hashxrcl  12571  hashdifsn  12623  brfi1indlem  12682  snopiswrd  12714  repsdf2  12918  modfsummods  13902  fsum00  13907  incexc  13944  fprodsplit1f  14093  2ebits  14470  bitsinvp1  14472  lcmfunsnlem2lem1  14660  lcmfunsnlem2lem2  14661  lcmfunsnlem2  14662  coprmproddvdslem  14728  4sqlem19  14962  ramxrcl  15024  strlemor1  15266  mrcsncl  15567  acsfn1  15616  homaf  15974  dmcoass  16010  lubel  16417  gsumws1  16672  cycsubg2  16903  cntzsnval  17027  0frgp  17478  dpjidcl  17740  ablfac1eu  17755  lspsncl  18249  lspsnss  18262  lspsnid  18265  lpival  18518  lpiss  18523  lidldvgen  18528  znlidl  19153  frgpcyg  19193  frlmlbs  19404  mat1dimelbas  19545  mat1dimmul  19550  smadiadetglem2  19746  isneip  20170  neips  20178  opnneip  20184  maxlp  20212  restsn2  20236  leordtval2  20277  ist1-3  20414  ordtt1  20444  2ndcdisj2  20521  uffix  20985  neiflim  21038  ptcmplem5  21120  cnextfres1  21132  haustsms2  21200  ust0  21283  ustuqtop5  21309  dscopn  21637  icccmplem1  21889  bndth  22035  ovolsn  22497  icombl1  22565  plyun0  23200  coeeulem  23227  coeeu  23228  vieta1lem2  23313  aalioulem2  23338  taylfval  23363  perfectlem2  24207  istrkg2ld  24557  axlowdimlem7  25027  axlowdimlem10  25030  konigsberg  25764  hsn0elch  26950  chsupsn  27115  chsup0  27250  h1deoi  27251  h1dei  27252  h1did  27253  h1de2ctlem  27257  h1de2ci  27258  spansni  27259  spansnch  27262  elspansncl  27267  spansnpji  27280  spanunsni  27281  spanpr  27282  h1datomi  27283  spansnji  27348  h1da  28051  atom1d  28055  superpos  28056  disjun0  28254  esumnul  28918  esumcst  28933  hashf2  28954  esum2d  28963  measvuni  29085  cntnevol  29099  eulerpartlemt  29253  eulerpartlemmf  29257  eulerpartlemgh  29260  ballotlemfp1  29373  dfon2lem3  30480  altxpsspw  30793  bj-snglss  31609  poimirlem16  32001  poimirlem19  32004  poimirlem23  32008  poimirlem25  32010  poimirlem26  32011  poimirlem29  32014  poimirlem31  32016  mblfinlem2  32023  dvasin  32073  fdc  32119  prnc  32345  isfldidl  32346  ispridlc  32348  islshpsm  32591  snatpsubN  33360  polatN  33541  atpsubclN  33555  pclfinclN  33560  mapfzcons  35603  mzpcompact2lem  35638  diophrw  35646  brfvidRP  36325  cotrcltrcl  36362  corcltrcl  36376  cotrclrcl  36379  binomcxplemnotnn0  36749  snelpwrVD  37267  disjiun2  37436  mapsnd  37514  mccllem  37715  islptre  37737  cncfdmsn  37806  snmbl  37878  stoweidlem44  37943  sge0tsms  38260  sge0iunmptlemfi  38293  ismeannd  38343  isomenndlem  38389  hoidmvlelem3  38457  hoidmvlelem4  38458  ovnhoilem1  38461  fnbrafvb  38694  afvres  38712  perfectALTVlem2  38882  nnsum3primesprm  38923  is01wlklem  39833  mapsnop  40399  lincext2  40521  snlindsntorlem  40536  aacllem  40813