Theorem snssi 3763

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 3753	. 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 2164   C_ wss 3154   {csn 3619

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3160  df-ss 3167  df-sn 3625

This theorem is referenced by:  difsnss  3765  sssnm  3781  tpssi  3786  snelpwi  4242  intid  4254  abnexg  4478  ordsucss  4537  xpsspw  4772  djussxp  4808  xpimasn  5115  fconst6g  5453  f1sng  5543  fvimacnvi  5673  fsn2  5733  fnressn  5745  fsnunf  5759  mapsn  6746  unsnfidcel  6979  en1eqsn  7009  exmidfodomrlemim  7263  axresscn  7922  nn0ssre  9247  1fv  10208  fxnn0nninf  10513  1exp  10642  hashdifsn  10893  hashdifpr  10894  fsum00  11608  hash2iun1dif1  11626  4sqlem19  12550  exmidunben  12586  lspsncl  13891  lspsnss  13903  lspsnid  13906  znlidl  14133  isneip  14325  neipsm  14333  opnneip  14338  plyun0  14915  plycjlemc  14938  plycj  14939  plyrecj  14941