Theorem snssi 2462

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

Syntax hints:   -> wi 3   e. wcel 956   (_ wss 2043  {csn 2405

This theorem is referenced by:  difsnid 2463  pwpw0 2465  snsspr 2466  sssn 2469  suceloni 3057  relsn 3249  xpsspw 3252  unixp0 3510  fvres 3725  fvimacnvi 3795  fvimacnvALT 3800  fsn2 3827  curry1 4088  map0 4334  mapsn 4335  fodomr 4469  mapdom2 4480  0sdom1dom 4510  abfii3 4543  pwfilem 4550  zfregs 4627  kmlem11 4755  axresscn 5248  supxrmnf 6042  nn0ssre 6058  caucvg3t 7112  ser1clim0 7117  ser1cmp0 7119  cvgcmp3cetlem1 7132  cvgcmp3cetlem2 7133  acdc3lem 7436  acdclem 7444  xpnnen 7449  ruclem39 7499  subbas2 7595  subtop 7596  isneip 7670  neips 7677  opnneip 7683  cnconst 7730  sncld 7737  lmconst 7886  metelcls 7916  bcth 7982  0oo 8394  ubthi 8488  hlim0 9044  hsn0elch 9059  chsupsn 9250  sh0let 9302  chsup0 9409  h1deot 9410  h1det 9411  h1did 9412  h1de2b 9415  h1de2bOLD 9416  h1de2ctlem 9417  h1de2ct 9418  spansn 9419  spansncht 9422  elspansnclt 9427  spansnpj 9441  spanunsn 9442  spanpr 9443  h1datom 9444  spansnj 9531  0cnfn 9843  0lnfn 9848  h1dat 10213  atom1d 10217  superpos 10218  fine 10384

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-in 2047  df-ss 2049  df-sn 2408

Copyright terms: Public domain