Theorem snssi 2470

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 2467	. 2 |- (A e. B -> (A e. B <-> {A} (_ B))
2	1	ibi 594	1 |- (A e. B -> {A} (_ B)

Syntax hints:   -> wi 3   e. wcel 960   (_ wss 2050  {csn 2413

This theorem is referenced by:  difsnid 2471  pwpw0 2473  snsspr 2474  sssn 2477  pwsnALT 2505  suceloni 3068  relsn 3260  xpsspw 3263  unixp0 3524  fvres 3740  fvimacnvi 3810  fvimacnvALT 3815  fsn2 3842  curry1 4104  map0 4350  mapsn 4351  fodomr 4489  mapdom2 4500  0sdom1dom 4530  pwfilem 4577  pwfilemOLD 4578  zfregs 4657  kmlem11 4785  axresscn 5280  supxrmnf 6089  nn0ssre 6105  caucvg3t 7168  ser1clim0 7173  ser1cmp0 7175  cvgcmp3cetlem1 7188  cvgcmp3cetlem2 7189  acdc3lem 7487  acdclem 7495  xpnnen 7500  ruclem39 7549  subtop 7643  isneip 7717  neips 7724  opnneip 7730  cnconst 7777  sncld 7784  lmconst 7931  metelcls 7962  bcth 8029  0oo 8445  ubthi 8540  hlim0 9100  hsn0elch 9115  chsupsn 9307  sh0let 9359  chsup0 9466  h1deot 9467  h1det 9468  h1did 9469  h1de2b 9472  h1de2ctlem 9473  h1de2ct 9474  spansn 9475  spansncht 9478  elspansnclt 9483  spansnpj 9496  spanunsn 9497  spanpr 9498  h1datom 9499  spansnj 9586  0cnfn 9899  0lnfn 9904  h1dat 10271  atom1d 10275  superpos 10276  fine 10442  setwoe 10532

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-in 2054  df-ss 2056  df-sn 2416

Copyright terms: Public domain