Theorem snssi 3854

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 3844	. 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 2209   C_ wss 3220   {csn 3705

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-sn 3711

This theorem is referenced by:  difsnss  3856  sssnm  3874  tpssi  3879  snelpwi  4346  intid  4359  abnexg  4587  ordsucss  4646  xpsspw  4882  djussxp  4920  xpimasn  5231  fconst6g  5586  f1sng  5678  fvimacnvi  5814  fsn2  5873  fnressn  5892  fsnunf  5906  ressuppss  6484  mapsnd  6960  mapsn  6962  unsnfidcel  7218  en1eqsn  7255  exmidfodomrlemim  7543  axresscn  8217  nn0ssre  9546  1fv  10524  fxnn0nninf  10854  1exp  10983  hashdifsn  11238  hashdifpr  11239  fsum00  12207  hash2iun1dif1  12225  4sqlem19  13166  ballotfilemfp1  13209  exmidunben  13295  lspsncl  14701  lspsnss  14713  lspsnid  14716  znlidl  14941  isneip  15170  neipsm  15178  opnneip  15183  plyun0  15760  plycjlemc  15784  plycj  15785  plyrecj  15787  dvply2g  15790  perfectlem2  16028