Theorem snssd 4776

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 4775	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3917  {csn 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-sn 4593

This theorem is referenced by:  intidg  5420  sofld  6163  fsnex  7261  fr3nr  7751  resf1extb  7913  resf1ext2b  7914  frrlem13  8280  oeeui  8569  naddunif  8660  naddasslem1  8661  naddasslem2  8662  ecinxp  8768  ralxpmap  8872  xpdom3  9044  domunsn  9097  mapdom3  9119  isinf  9214  isinfOLD  9215  ac6sfi  9238  pwfilem  9274  finsschain  9317  ssfii  9377  marypha1lem  9391  unxpwdom2  9548  en2other2  9969  fseqenlem1  9984  axdc3lem4  10413  axdc4lem  10415  ttukeylem7  10475  fpwwe2lem12  10602  canthwe  10611  canthp1lem1  10612  wuncval2  10707  un0addcl  12482  un0mulcl  12483  ssfzunsnext  13537  fseq1p1m1  13566  hashbclem  14424  hashf1lem1  14427  fsumsplit1  15718  fsumge1  15770  incexclem  15809  isumltss  15821  fprodsplit1f  15963  rpnnen2lem11  16199  bitsinv1  16419  lcmfunsnlem2  16617  lcmfass  16623  phicl2  16745  vdwlem1  16959  vdwlem8  16966  vdwlem12  16970  vdwlem13  16971  0ram  16998  ramub1lem1  17004  ramub1lem2  17005  ramcl  17007  imasaddfnlem  17498  imasaddflem  17500  imasvscafn  17507  imasvscaf  17509  mrieqvlemd  17597  mreexmrid  17611  mreexexlem4d  17615  acsfiindd  18519  acsmapd  18520  gsumress  18616  0subm  18751  gsumvallem2  18768  0subgOLD  19091  trivsubgd  19092  trivsubgsnd  19093  trivnsgd  19111  cycsubg2cl  19150  kerf1ghm  19186  pmtrprfv  19390  odf1o1  19509  gex1  19528  sylow2alem1  19554  sylow2alem2  19555  lsm01  19608  lsm02  19609  lsmdisj  19618  lsmdisj2  19619  prmcyg  19831  gsumzadd  19859  gsumconst  19871  gsumdifsnd  19898  gsumpt  19899  gsumxp  19913  dmdprdd  19938  dprdfadd  19959  dprdres  19967  dprdz  19969  dprdsn  19975  dprddisj2  19978  dprd2da  19981  dprd2d2  19983  dmdprdsplit2lem  19984  dpjcntz  19991  dpjdisj  19992  dpjlsm  19993  dpjidcl  19997  ablfacrp  20005  ablfac1eu  20012  pgpfac1lem1  20013  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfac1lem5  20018  pgpfaclem2  20021  acsfn1p  20715  lsssn0  20861  lss0ss  20862  lsptpcl  20892  lspsnvsi  20917  lspun0  20924  pwssplit1  20973  lsmpr  21003  lsppr  21007  lspsntri  21011  lspsolvlem  21059  lspsolv  21060  lsppratlem1  21064  lsppratlem3  21066  lsppratlem4  21067  islbs3  21072  lbsextlem4  21078  rnglidl0  21146  rsp1  21154  lidlnz  21159  lidldvgen  21251  mulgrhm2  21395  zndvds  21466  psrlidm  21878  psrridm  21879  mplmonmul  21950  mdetdiaglem  22492  mdetrlin  22496  mdetrsca  22497  mdetrsca2  22498  mdetrlin2  22501  mdetunilem5  22510  mdetunilem9  22514  mdetmul  22517  en2top  22879  rest0  23063  ordtrest  23096  iscnp4  23157  cnconst2  23177  cnpdis  23187  ist1-2  23241  cnt1  23244  dishaus  23276  discmp  23292  cmpcld  23296  conncompid  23325  dis2ndc  23354  dislly  23391  dissnref  23422  comppfsc  23426  llycmpkgen2  23444  cmpkgen  23445  1stckgenlem  23447  1stckgen  23448  ptbasfi  23475  txdis  23526  txdis1cn  23529  txcmplem1  23535  xkohaus  23547  xkoptsub  23548  xkoinjcn  23581  snfbas  23760  trnei  23786  isufil2  23802  ufileu  23813  filufint  23814  uffixsn  23819  ufildom1  23820  flimopn  23869  hausflim  23875  flimcf  23876  flimclslem  23878  flimsncls  23880  cnpflf2  23894  cnpflf  23895  fclsneii  23911  fclsfnflim  23921  fcfnei  23929  flfcntr  23937  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem2  23947  cldsubg  24005  snclseqg  24010  qustgphaus  24017  tsmsgsum  24033  tsmsid  24034  tgptsmscld  24045  tsmsxplem1  24047  tsmsxplem2  24048  ust0  24114  ustuqtop1  24136  neipcfilu  24190  prdsdsf  24262  prdsxmetlem  24263  prdsmet  24265  imasdsf1olem  24268  xpsdsval  24276  prdsbl  24386  prdsxmslem2  24424  idnghm  24638  icccmplem2  24719  metnrmlem2  24756  ioombl  25473  volivth  25515  itg11  25599  i1fmulclem  25610  itg2mulclem  25654  itgsplitioo  25746  limcvallem  25779  limcdif  25784  ellimc2  25785  limcflf  25789  limcmpt2  25792  limcres  25794  cnplimc  25795  limccnp  25799  limccnp2  25800  limcco  25801  dvreslem  25817  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  dvcmulf  25855  dvef  25891  dvivth  25922  lhop2  25927  lhop  25928  ply1remlem  26077  fta1blem  26083  ig1peu  26087  ig1pdvds  26092  plyco0  26104  elply2  26108  plyf  26110  elplyr  26113  elplyd  26114  ply1term  26116  ply0  26120  plyeq0lem  26122  plyeq0  26123  plypf1  26124  plyaddlem  26127  plymullem  26128  dgrlem  26141  coef2  26143  coeidlem  26149  plyco  26153  coemulhi  26166  plycj  26190  plycjOLD  26192  vieta1  26227  taylf  26275  radcnv0  26332  abelth  26358  rlimcnp  26882  xrlimcnp  26885  amgm  26908  wilthlem2  26986  basellem7  27004  basellem9  27006  ppiprm  27068  chtprm  27070  musumsum  27109  muinv  27110  logexprlim  27143  perfectlem2  27148  dchrhash  27189  rpvmasum2  27430  ssltsn  27711  slerec  27738  cofcutr  27839  cutlt  27847  cutmax  27849  cutmin  27850  addsuniflem  27915  negsunif  27968  ssltmul1  28057  ssltmul2  28058  precsexlem11  28126  onscutlt  28172  n0sfincut  28253  0reno  28355  axlowdimlem7  28882  axlowdimlem10  28885  upgrex  29026  upgr1elem  29046  uvtxnm1nbgr  29338  umgr2v2e  29460  cyclnumvtx  29737  0oo  30725  sh0le  31376  disjiunel  32532  preimane  32601  fnpreimac  32602  fsuppinisegfi  32617  fprodeq02  32755  s1f1  32871  gsumzresunsn  33003  gsumhashmul  33008  pmtrcnelor  33055  primefldgen1  33278  dvdsrspss  33365  elgrplsmsn  33368  lsmsnorb  33369  grplsm0l  33381  grplsmid  33382  0ringidl  33399  unitpidl1  33402  elrspunsn  33407  drngidl  33411  isprmidlc  33425  qsidomlem2  33431  ssdifidlprm  33436  mxidlprm  33448  mxidlirredi  33449  mxidlirred  33450  drngmxidl  33455  drngmxidlr  33456  qsdrngilem  33472  rsprprmprmidl  33500  rprmirredb  33510  1arithufdlem4  33525  lsatdim  33620  drngdimgt0  33621  dimkerim  33630  evls1fldgencl  33672  algextdeglem1  33714  algextdeglem2  33715  algextdeglem3  33716  algextdeglem4  33717  algextdeglem5  33718  rtelextdg2  33724  constrextdg2lem  33745  constrext2chnlem  33747  constrfiss  33748  qtopt1  33832  locfinref  33838  zarcls0  33865  zarmxt1  33877  zarcmplem  33878  ordtrestNEW  33918  esumsnf  34061  esum2dlem  34089  rossros  34177  oms0  34295  carsggect  34316  eulerpartlems  34358  eulerpartlemgc  34360  eulerpartlemgh  34376  eulerpartlemgs2  34378  plymulx0  34545  circlemeth  34638  hgt750lemb  34654  hgt750leme  34656  bnj1452  35049  pthhashvtx  35122  subfacp1lem1  35173  subfacp1lem5  35178  erdszelem4  35188  erdszelem8  35192  sconnpi1  35233  cvmscld  35267  cvmlift2lem6  35302  cvmlift2lem9  35305  cvmlift2lem11  35307  cvmlift2lem12  35308  mrsubvrs  35516  ellcsrspsn  35635  neibastop2lem  36355  topjoin  36360  fnejoin2  36364  weiunse  36463  pibt2  37412  lindsadd  37614  poimirlem3  37624  poimirlem9  37630  poimirlem28  37649  poimirlem32  37653  prdsbnd  37794  heiborlem8  37819  rrnequiv  37836  grpokerinj  37894  0idl  38026  prnc  38068  isfldidl  38069  lshpnel2N  38985  lsatfixedN  39009  lfl0f  39069  lkrlsp3  39104  elpaddatriN  39804  elpaddat  39805  elpadd2at  39807  pmodlem1  39847  osumcllem1N  39957  osumcllem2N  39958  osumcllem9N  39965  osumcllem10N  39966  pexmidlem6N  39976  pexmidlem7N  39977  dibss  41170  dochocsn  41382  dochsncom  41383  dochnel  41394  dihprrnlem1N  41425  dihprrnlem2  41426  djhlsmat  41428  dihsmsprn  41431  dvh4dimlem  41444  dvhdimlem  41445  dochsnnz  41451  dochsatshp  41452  dochsnshp  41454  dochexmid  41469  dochsnkr  41473  dochsnkr2cl  41475  dochfl1  41477  lcfl7lem  41500  lcfl6  41501  lcfl8  41503  lcfl9a  41506  lclkrlem2a  41508  lclkrlem2c  41510  lclkrlem2d  41511  lclkrlem2e  41512  lclkrlem2j  41517  lclkrlem2o  41522  lclkrlem2p  41523  lclkrlem2s  41526  lclkrlem2v  41529  lcfrlem14  41557  lcfrlem18  41561  lcfrlem19  41562  lcfrlem20  41563  lcfrlem23  41566  lcfrlem25  41568  lcdlkreqN  41623  mapdval4N  41633  mapdsn  41642  mapdhvmap  41770  hdmaprnlem4tN  41853  hdmapinvlem1  41919  hdmapinvlem2  41920  hdmapinvlem3  41921  hdmapinvlem4  41922  hdmapglem5  41923  hgmapvvlem3  41926  hdmapglem7a  41928  hdmapglem7b  41929  hdmapglem7  41930  hdmapoc  41932  aks6d1c5lem3  42132  deg1gprod  42135  sticksstones9  42149  sticksstones11  42151  rhmqusspan  42180  evlsbagval  42561  selvvvval  42580  0prjspnrel  42622  elrfi  42689  cmpfiiin  42692  mzpcompact2lem  42746  dfac11  43058  pwssplit4  43085  rngunsnply  43165  flcidc  43166  proot1mul  43190  iocinico  43208  cantnfresb  43320  iunrelexp0  43698  frege81d  43743  k0004lem3  44145  mnuunid  44273  binomcxplemnn0  44345  islptre  45624  limciccioolb  45626  limcicciooub  45642  limcresiooub  45647  limcresioolb  45648  ioccncflimc  45890  icccncfext  45892  icocncflimc  45894  cncfiooicc  45899  dvnprodlem2  45952  dirkercncflem2  46109  dirkercncflem3  46110  fourierdlem48  46159  fourierdlem49  46160  fourierdlem79  46190  fourierdlem101  46212  sge0sup  46396  hoidmvlelem2  46601  hoiqssbl  46630  hspmbllem1  46631  hspmbllem2  46632  ovnovollem1  46661  fsumsplitsndif  47378  imaelsetpreimafv  47400  perfectALTVlem2  47727  stgrclnbgr0  47968  isubgr3stgrlem3  47971  1hegrlfgr  48124  gsumdifsndf  48173  sepfsepc  48920  discsubc  49057  iinfconstbas  49059