Theorem snssi 3812

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 3802	. 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 2200   C_ wss 3197   {csn 3666

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-in 3203  df-ss 3210  df-sn 3672

This theorem is referenced by:  difsnss  3814  sssnm  3832  tpssi  3837  snelpwi  4297  intid  4310  abnexg  4537  ordsucss  4596  xpsspw  4831  djussxp  4867  xpimasn  5177  fconst6g  5524  f1sng  5615  fvimacnvi  5749  fsn2  5809  fnressn  5825  fsnunf  5839  mapsn  6837  unsnfidcel  7083  en1eqsn  7115  exmidfodomrlemim  7379  axresscn  8047  nn0ssre  9373  1fv  10335  fxnn0nninf  10661  1exp  10790  hashdifsn  11041  hashdifpr  11042  fsum00  11973  hash2iun1dif1  11991  4sqlem19  12932  exmidunben  12997  lspsncl  14356  lspsnss  14368  lspsnid  14371  znlidl  14598  isneip  14820  neipsm  14828  opnneip  14833  plyun0  15410  plycjlemc  15434  plycj  15435  plyrecj  15437  dvply2g  15440  perfectlem2  15674