Theorem snssi 3129

Description: The singleton of an element of a class is a subset of the class.

Assertion

Ref	Expression
snssi	|- (A e. B -> {A} C_ B)

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 3124	. 2 |- (A e. B -> (A e. B <-> {A} C_ B))
2	1	ibi 652	1 |- (A e. B -> {A} C_ B)

Syntax hints:   -> wi 3   e. wcel 1300   C_ wss 2593  {csn 3044

This theorem is referenced by:  difsnid 3131  pwpw0 3134  sssn 3142  pwsnALT 3173  intid 3512  suceloni 3894  relsn 4087  xpsspw 4093  unixp0 4423  fvres 4691  nfunsnOLD 4707  dffv2 4734  fvimacnvi 4777  fvimacnvALT 4782  fsn2 4809  curry1 5075  curry2 5078  map0 5403  mapsn 5404  fodomr 5547  mapdom2 5588  0sdom1dom 5618  abfii3 5653  zfregs 5754  kmlem11 5937  axresscn 6420  axresscnOLD 6421  supxrmnf 7296  nn0ssre 7312  caucvg3 8428  ser1clim0 8433  ser1cmp0i 8435  cvgcmp3cetlem1 8449  cvgcmp3cetlem2 8450  acdc3lem 8754  acdclem 8763  xpnnen 8768  ruclem39 8817  subbas2 8915  subtop 8916  isneip 8996  neips 9003  opnneip 9009  cnconst 9057  sncld 9064  lmconst 9212  metelcls 9243  bcth 9310  0oo 9789  ubthi 9889  setwoe 10170  dif1enOLD 10173  indexfi 10174  fine 10213  hausfillim 10303  flimopn 10321  hlim0 10738  hsn0elch 10753  chsupsn 10945  chsup0 11104  h1deoi 11105  h1dei 11106  h1did 11107  h1de2bi 11110  h1de2ctlem 11111  h1de2ci 11112  spansni 11113  spansnch 11116  elspansncl 11121  spansnpji 11134  spanunsni 11135  spanpr 11136  h1datomi 11137  spansnji 11226  0cnfn 11541  0lnfn 11546  opsqrlem3 11713  h1da 11921  atom1d 11925  superpos 11926  algrf 13739  domrancur1c 14550  osneisi 14875  subtopsin2 14907  limfilnei 14943  conttnf 14944  conttnf2 14945  iscnp3 14946  cnpfillim4 14947  tarsuc1 15244  inficlALT 15372  finsschain 15373  compfipin0 15436  comppfsc 15517  ist1-2 15542  ist1-3 15543  uffixfr 15575  fixufil 15576  neiplim 15586  limfilcf 15587  flimcls 15588  cnpfillim 15589  fconst6 15700  findcard2 15745  indexfiOLD 15755  frfi 15771  fdc 15812  tlmconst 15907  heiborlem18 15972  heiborlem38 15992  heiborlem42 15996  reheibor 16025  prnc 16215  isfldidl 16216  ispridlc 16218  snelpwrVD 16654  snelpwr 16655  lubel 16898  pointpsub 17231  polat 17341  atpsubcl 17354

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294  df-in 2603  df-ss 2605  df-sn 3049

Copyright terms: Public domain