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  5457  f1sng  5547  fvimacnvi  5677  fsn2  5737  fnressn  5749  fsnunf  5763  mapsn  6750  unsnfidcel  6983  en1eqsn  7015  exmidfodomrlemim  7270  axresscn  7929  nn0ssre  9255  1fv  10216  fxnn0nninf  10533  1exp  10662  hashdifsn  10913  hashdifpr  10914  fsum00  11629  hash2iun1dif1  11647  4sqlem19  12588  exmidunben  12653  lspsncl  13958  lspsnss  13970  lspsnid  13973  znlidl  14200  isneip  14392  neipsm  14400  opnneip  14405  plyun0  14982  plycjlemc  15006  plycj  15007  plyrecj  15009  dvply2g  15012  perfectlem2  15246