Theorem snssi 1851

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

Assertion

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

Proof of Theorem snssi

Step	Hyp	Ref	Expression
1		snssg 1850	. 2 |- (A e. B -> (A e. B <-> {A} (_ B))
2	1	ibi 449	1 |- (A e. B -> {A} (_ B)

Syntax hints:   -> wi 2   e. wcel 1092   (_ wss 1487  {csn 1808

This theorem is referenced by:  sssn 1852  snsspr 1853  suceloni 2314  relsn 2485  xpex 2488  fvres 2840  fsn2 2896  oe0m1 3129  map0 3268  mapsn 3269  mapdom2 3389  phplem1 3403  0sdom1dom 3420  pssnn 3428  zfregs 3491  kmlem10 3589  fodomb 3615  axresscn 4062  nn0ssre 4538  clim0 4882  ruclem39 4923  xpnnen 4927  hlim0 5140  hsn0elch 5155  chsupsn 5313  sh0let 5365  chsup0 5453  h1deot 5454  h1det 5455  h1did 5456  h1de2b 5459  h1de2ctlem 5460  h1de2ct 5461  spansn 5462  spansncht 5465  spansnmul 5469  elspansnclt 5470  spansnpj 5481  spanunsn 5482  h1datom 5483  spansnj 5539  h1dat 5747  atom1d 5750

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-in 1491  df-ss 1492  df-sn 1811

metamath.org