Theorem snssi 2530

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

Assertion

Ref	Expression
snssi	⊢ (A ∈ B → {A} ⊆ B)

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 2527	. 2 ⊢ (A ∈ B → (A ∈ B ↔ {A} ⊆ B))
2	1	ibi 595	1 ⊢ (A ∈ B → {A} ⊆ B)

Syntax hints:   → wi 3   ∈ wcel 994   ⊆ wss 2099  {csn 2467

This theorem is referenced by:  difsnid 2531  pwpw0 2533  snsspr1 2534  sssn 2538  pwsnALT 2566  intid 2843  suceloni 3170  relsn 3343  xpsspw 3346  unixp0 3623  fvres 3845  fvimacnvi 3918  fvimacnvALT 3923  fsn2 3950  curry1 4193  curry2 4196  map0 4485  mapsn 4486  fodomr 4628  mapdom2 4641  0sdom1dom 4671  abfii3 4706  pwfilem 4713  zfregs 4793  kmlem11 4921  axresscn 5422  supxrmnf 6255  nn0ssre 6271  caucvg3 7371  ser1clim0 7376  ser1cmp0i 7378  cvgcmp3cetlem1 7392  cvgcmp3cetlem2 7393  acdc3lem 7697  acdclem 7706  xpnnen 7711  ruclem39 7760  subbas2 7857  subtop 7858  isneip 7930  neips 7937  opnneip 7943  cnconst 7990  sncld 7997  lmconst 8145  metelcls 8176  bcth 8243  0oo 8704  ubthi 8804  hlim0 9381  hsn0elch 9396  chsupsn 9588  sh0le 9640  chsup0 9747  h1deoi 9748  h1dei 9749  h1did 9750  h1de2bi 9753  h1de2ctlem 9754  h1de2ci 9755  spansni 9756  spansnch 9759  elspansncl 9764  spansnpji 9777  spanunsni 9778  spanpr 9779  h1datomi 9780  spansnji 9869  0cnfn 10183  0lnfn 10188  h1da 10557  atom1d 10561  superpos 10562  fine 10736  setwoe 10828  osneisi 11018  subtopsin2 11067  inficlALT 11424  finsschain 11425  cptclsscpt 11489  compfipin0 11493  alexsublem3 11498  alexsublem4 11499  comppfsc 11578  ist1-2 11603  ist1-3 11604  uffixfr 11660  fixufil 11661  flimopn 11679  neiplim 11681  limfilcf 11683  flimcls 11684  hausfillim 11685  cnpfillim 11686  fclsfnflim 11726  dif1en 11833  indexf 11847  fsumleisumi 11889  tlmconst 11968  heiborlem18 12028  heiborlem38 12048  heiborlem42 12052  bfplem1 12054  bfplem11 12064  bfp 12065  reheibor 12081

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-in 2103  df-ss 2105  df-sn 2470

Copyright terms: Public domain