Theorem snssi 3777

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 3767	. 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 2176   C_ wss 3166   {csn 3633

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-in 3172  df-ss 3179  df-sn 3639

This theorem is referenced by:  difsnss  3779  sssnm  3795  tpssi  3800  snelpwi  4257  intid  4269  abnexg  4494  ordsucss  4553  xpsspw  4788  djussxp  4824  xpimasn  5132  fconst6g  5476  f1sng  5566  fvimacnvi  5696  fsn2  5756  fnressn  5772  fsnunf  5786  mapsn  6779  unsnfidcel  7020  en1eqsn  7052  exmidfodomrlemim  7311  axresscn  7975  nn0ssre  9301  1fv  10263  fxnn0nninf  10586  1exp  10715  hashdifsn  10966  hashdifpr  10967  fsum00  11806  hash2iun1dif1  11824  4sqlem19  12765  exmidunben  12830  lspsncl  14187  lspsnss  14199  lspsnid  14202  znlidl  14429  isneip  14651  neipsm  14659  opnneip  14664  plyun0  15241  plycjlemc  15265  plycj  15266  plyrecj  15268  dvply2g  15271  perfectlem2  15505