Theorem snssd 4739

Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
snssd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Assertion

Ref	Expression
snssd	⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd

Step	Hyp	Ref	Expression
1		snssd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		snssi 4738	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900  df-sn 4559

This theorem is referenced by:  sofld  6079  fsnex  7135  fr3nr  7600  frrlem13  8085  wfrlem15OLD  8125  oeeui  8395  ecinxp  8539  ralxpmap  8642  xpdom3  8810  domunsn  8863  mapdom3  8885  pwfilem  8922  isinf  8965  ac6sfi  8988  pwfilemOLD  9043  finsschain  9056  ssfii  9108  marypha1lem  9122  unxpwdom2  9277  en2other2  9696  fseqenlem1  9711  axdc3lem4  10140  axdc4lem  10142  ttukeylem7  10202  fpwwe2lem12  10329  canthwe  10338  canthp1lem1  10339  wuncval2  10434  un0addcl  12196  un0mulcl  12197  ssfzunsnext  13230  fseq1p1m1  13259  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  fsumsplit1  15385  fsumge1  15437  incexclem  15476  isumltss  15488  fprodsplit1f  15628  rpnnen2lem11  15861  bitsinv1  16077  lcmfunsnlem2  16273  lcmfass  16279  phicl2  16397  vdwlem1  16610  vdwlem8  16617  vdwlem12  16621  vdwlem13  16622  0ram  16649  ramub1lem1  16655  ramub1lem2  16656  ramcl  16658  imasaddfnlem  17156  imasaddflem  17158  imasvscafn  17165  imasvscaf  17167  mrieqvlemd  17255  mreexmrid  17269  mreexexlem4d  17273  acsfiindd  18186  acsmapd  18187  gsumress  18281  0subm  18371  gsumvallem2  18387  0subg  18695  trivsubgd  18696  trivsubgsnd  18697  trivnsgd  18715  cycsubg2cl  18745  pmtrprfv  18976  odf1o1  19092  gex1  19111  sylow2alem1  19137  sylow2alem2  19138  lsm01  19192  lsm02  19193  lsmdisj  19202  lsmdisj2  19203  prmcyg  19410  gsumzadd  19438  gsumconst  19450  gsumdifsnd  19477  gsumpt  19478  gsumxp  19492  dmdprdd  19517  dprdfadd  19538  dprdres  19546  dprdz  19548  dprdsn  19554  dprddisj2  19557  dprd2da  19560  dprd2d2  19562  dmdprdsplit2lem  19563  dpjcntz  19570  dpjdisj  19571  dpjlsm  19572  dpjidcl  19576  ablfacrp  19584  ablfac1eu  19591  pgpfac1lem1  19592  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem5  19597  pgpfaclem2  19600  kerf1ghm  19902  acsfn1p  19982  lsssn0  20124  lss0ss  20125  lsptpcl  20156  lspsnvsi  20181  lspun0  20188  pwssplit1  20236  lsmpr  20266  lsppr  20270  lspsntri  20274  lspsolvlem  20319  lspsolv  20320  lsppratlem1  20324  lsppratlem3  20326  lsppratlem4  20327  islbs3  20332  lbsextlem4  20338  rsp1  20408  lidlnz  20412  lidldvgen  20439  mulgrhm2  20612  zndvds  20669  psrlidm  21082  psrridm  21083  mplmonmul  21147  mdetdiaglem  21655  mdetrlin  21659  mdetrsca  21660  mdetrsca2  21661  mdetrlin2  21664  mdetunilem5  21673  mdetunilem9  21677  mdetmul  21680  en2top  22043  rest0  22228  ordtrest  22261  iscnp4  22322  cnconst2  22342  cnpdis  22352  ist1-2  22406  cnt1  22409  dishaus  22441  discmp  22457  cmpcld  22461  conncompid  22490  dis2ndc  22519  dislly  22556  dissnref  22587  comppfsc  22591  llycmpkgen2  22609  cmpkgen  22610  1stckgenlem  22612  1stckgen  22613  ptbasfi  22640  txdis  22691  txdis1cn  22694  txcmplem1  22700  xkohaus  22712  xkoptsub  22713  xkoinjcn  22746  snfbas  22925  trnei  22951  isufil2  22967  ufileu  22978  filufint  22979  uffixsn  22984  ufildom1  22985  flimopn  23034  hausflim  23040  flimcf  23041  flimclslem  23043  flimsncls  23045  cnpflf2  23059  cnpflf  23060  fclsneii  23076  fclsfnflim  23086  fcfnei  23094  flfcntr  23102  alexsubALTlem3  23108  alexsubALTlem4  23109  ptcmplem2  23112  cldsubg  23170  snclseqg  23175  qustgphaus  23182  tsmsgsum  23198  tsmsid  23199  tgptsmscld  23210  tsmsxplem1  23212  tsmsxplem2  23213  ust0  23279  ustuqtop1  23301  neipcfilu  23356  prdsdsf  23428  prdsxmetlem  23429  prdsmet  23431  imasdsf1olem  23434  xpsdsval  23442  prdsbl  23553  prdsxmslem2  23591  idnghm  23813  icccmplem2  23892  metnrmlem2  23929  ioombl  24634  volivth  24676  itg11  24760  i1fmulclem  24772  itg2mulclem  24816  itgsplitioo  24907  limcvallem  24940  limcdif  24945  ellimc2  24946  limcflf  24950  limcmpt2  24953  limcres  24955  cnplimc  24956  limccnp  24960  limccnp2  24961  limcco  24962  dvreslem  24978  dvaddbr  25007  dvmulbr  25008  dvcmulf  25014  dvef  25049  dvivth  25079  lhop2  25084  lhop  25085  ply1remlem  25232  fta1blem  25238  ig1peu  25241  ig1pdvds  25246  plyco0  25258  elply2  25262  plyf  25264  elplyr  25267  elplyd  25268  ply1term  25270  ply0  25274  plyeq0lem  25276  plyeq0  25277  plypf1  25278  plyaddlem  25281  plymullem  25282  dgrlem  25295  coef2  25297  coeidlem  25303  plyco  25307  coemulhi  25320  plycj  25343  vieta1  25377  taylf  25425  radcnv0  25480  abelth  25505  rlimcnp  26020  xrlimcnp  26023  amgm  26045  wilthlem2  26123  basellem7  26141  basellem9  26143  ppiprm  26205  chtprm  26207  musumsum  26246  muinv  26247  logexprlim  26278  perfectlem2  26283  dchrhash  26324  rpvmasum2  26565  axlowdimlem7  27219  axlowdimlem10  27222  upgrex  27365  upgr1elem  27385  uvtxnm1nbgr  27674  umgr2v2e  27795  0oo  29052  sh0le  29703  disjiunel  30836  preimane  30909  fnpreimac  30910  fsuppinisegfi  30923  fprodeq02  31039  s1f1  31119  gsumzresunsn  31216  gsumhashmul  31218  pmtrcnelor  31262  elgrplsmsn  31480  lsmsnorb  31481  grplsm0l  31493  grplsmid  31494  0ringidl  31507  isprmidlc  31525  qsidomlem2  31531  mxidlprm  31542  lsatdim  31602  drngdimgt0  31603  dimkerim  31610  qtopt1  31687  locfinref  31693  zarcls0  31720  zarmxt1  31732  zarcmplem  31733  ordtrestNEW  31773  esumsnf  31932  esum2dlem  31960  rossros  32048  oms0  32164  carsggect  32185  eulerpartlems  32227  eulerpartlemgc  32229  eulerpartlemgh  32245  eulerpartlemgs2  32247  plymulx0  32426  circlemeth  32520  hgt750lemb  32536  hgt750leme  32538  bnj1452  32932  pthhashvtx  32989  subfacp1lem1  33041  subfacp1lem5  33046  erdszelem4  33056  erdszelem8  33060  sconnpi1  33101  cvmscld  33135  cvmlift2lem6  33170  cvmlift2lem9  33173  cvmlift2lem11  33175  cvmlift2lem12  33176  mrsubvrs  33384  slerec  33940  cofcutr  34019  neibastop2lem  34476  topjoin  34481  fnejoin2  34485  pibt2  35515  lindsadd  35697  poimirlem3  35707  poimirlem9  35713  poimirlem28  35732  poimirlem32  35736  prdsbnd  35878  heiborlem8  35903  rrnequiv  35920  grpokerinj  35978  0idl  36110  prnc  36152  isfldidl  36153  lshpnel2N  36926  lsatfixedN  36950  lfl0f  37010  lkrlsp3  37045  elpaddatriN  37744  elpaddat  37745  elpadd2at  37747  pmodlem1  37787  osumcllem1N  37897  osumcllem2N  37898  osumcllem9N  37905  osumcllem10N  37906  pexmidlem6N  37916  pexmidlem7N  37917  dibss  39110  dochocsn  39322  dochsncom  39323  dochnel  39334  dihprrnlem1N  39365  dihprrnlem2  39366  djhlsmat  39368  dihsmsprn  39371  dvh4dimlem  39384  dvhdimlem  39385  dochsnnz  39391  dochsatshp  39392  dochsnshp  39394  dochexmid  39409  dochsnkr  39413  dochsnkr2cl  39415  dochfl1  39417  lcfl7lem  39440  lcfl6  39441  lcfl8  39443  lcfl9a  39446  lclkrlem2a  39448  lclkrlem2c  39450  lclkrlem2d  39451  lclkrlem2e  39452  lclkrlem2j  39457  lclkrlem2o  39462  lclkrlem2p  39463  lclkrlem2s  39466  lclkrlem2v  39469  lcfrlem14  39497  lcfrlem18  39501  lcfrlem19  39502  lcfrlem20  39503  lcfrlem23  39506  lcfrlem25  39508  lcdlkreqN  39563  mapdval4N  39573  mapdsn  39582  mapdhvmap  39710  hdmaprnlem4tN  39793  hdmapinvlem1  39859  hdmapinvlem2  39860  hdmapinvlem3  39861  hdmapinvlem4  39862  hdmapglem5  39863  hgmapvvlem3  39866  hdmapglem7a  39868  hdmapglem7b  39869  hdmapglem7  39870  hdmapoc  39872  sticksstones9  40038  sticksstones11  40040  evlsbagval  40198  0prjspnrel  40385  elrfi  40432  cmpfiiin  40435  mzpcompact2lem  40489  dfac11  40803  pwssplit4  40830  rngunsnply  40914  flcidc  40915  proot1mul  40940  iocinico  40959  iunrelexp0  41199  frege81d  41244  k0004lem3  41648  mnuunid  41784  binomcxplemnn0  41856  islptre  43050  limciccioolb  43052  limcicciooub  43068  limcresiooub  43073  limcresioolb  43074  ioccncflimc  43316  icccncfext  43318  icocncflimc  43320  cncfiooicc  43325  dvnprodlem2  43378  dirkercncflem2  43535  dirkercncflem3  43536  fourierdlem48  43585  fourierdlem49  43586  fourierdlem79  43616  fourierdlem101  43638  sge0sup  43819  hoidmvlelem2  44024  hoiqssbl  44053  hspmbllem1  44054  hspmbllem2  44055  ovnovollem1  44084  fsumsplitsndif  44713  imaelsetpreimafv  44735  perfectALTVlem2  45062  1hegrlfgr  45182  gsumdifsndf  45263  sepfsepc  46109