Theorem snssi 3767

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

Syntax hints:   -> wi 4   e. wcel 2167   C_ wss 3157   {csn 3623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170  df-sn 3629

This theorem is referenced by:  difsnss  3769  sssnm  3785  tpssi  3790  snelpwi  4246  intid  4258  abnexg  4482  ordsucss  4541  xpsspw  4776  djussxp  4812  xpimasn  5119  fconst6g  5459  f1sng  5549  fvimacnvi  5679  fsn2  5739  fnressn  5751  fsnunf  5765  mapsn  6758  unsnfidcel  6991  en1eqsn  7023  exmidfodomrlemim  7280  axresscn  7944  nn0ssre  9270  1fv  10231  fxnn0nninf  10548  1exp  10677  hashdifsn  10928  hashdifpr  10929  fsum00  11644  hash2iun1dif1  11662  4sqlem19  12603  exmidunben  12668  lspsncl  14024  lspsnss  14036  lspsnid  14039  znlidl  14266  isneip  14466  neipsm  14474  opnneip  14479  plyun0  15056  plycjlemc  15080  plycj  15081  plyrecj  15083  dvply2g  15086  perfectlem2  15320