Theorem snssi 3748

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 3738	. 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 2158   C_ wss 3141   {csn 3604

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-v 2751  df-in 3147  df-ss 3154  df-sn 3610

This theorem is referenced by:  difsnss  3750  sssnm  3766  tpssi  3771  snelpwi  4224  intid  4236  abnexg  4458  ordsucss  4515  xpsspw  4750  djussxp  4784  xpimasn  5089  fconst6g  5426  f1sng  5515  fvimacnvi  5643  fsn2  5703  fnressn  5715  fsnunf  5729  mapsn  6704  unsnfidcel  6934  en1eqsn  6961  exmidfodomrlemim  7214  axresscn  7873  nn0ssre  9194  1fv  10153  fxnn0nninf  10452  1exp  10563  hashdifsn  10813  hashdifpr  10814  fsum00  11484  hash2iun1dif1  11502  exmidunben  12441  lspsncl  13638  lspsnss  13650  lspsnid  13653  znlidl  13849  isneip  13999  neipsm  14007  opnneip  14012