Theorem snssd 4765

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3901  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-sn 4581

This theorem is referenced by:  intidg  5405  sofld  6145  fsnex  7229  fr3nr  7717  resf1extb  7876  resf1ext2b  7877  frrlem13  8240  oeeui  8530  naddunif  8621  naddasslem1  8622  naddasslem2  8623  ecinxp  8729  ralxpmap  8834  xpdom3  9003  domunsn  9055  mapdom3  9077  isinf  9165  ac6sfi  9184  pwfilem  9218  finsschain  9259  ssfii  9322  marypha1lem  9336  unxpwdom2  9493  en2other2  9919  fseqenlem1  9934  axdc3lem4  10363  axdc4lem  10365  ttukeylem7  10425  fpwwe2lem12  10553  canthwe  10562  canthp1lem1  10563  wuncval2  10658  un0addcl  12434  un0mulcl  12435  ssfzunsnext  13485  fseq1p1m1  13514  hashbclem  14375  hashf1lem1  14378  fsumsplit1  15668  fsumge1  15720  incexclem  15759  isumltss  15771  fprodsplit1f  15913  rpnnen2lem11  16149  bitsinv1  16369  lcmfunsnlem2  16567  lcmfass  16573  phicl2  16695  vdwlem1  16909  vdwlem8  16916  vdwlem12  16920  vdwlem13  16921  0ram  16948  ramub1lem1  16954  ramub1lem2  16955  ramcl  16957  imasaddfnlem  17449  imasaddflem  17451  imasvscafn  17458  imasvscaf  17460  mrieqvlemd  17552  mreexmrid  17566  mreexexlem4d  17570  acsfiindd  18476  acsmapd  18477  chnccat  18549  gsumress  18607  0subm  18742  gsumvallem2  18759  trivsubgd  19082  trivsubgsnd  19083  trivnsgd  19101  cycsubg2cl  19140  kerf1ghm  19176  pmtrprfv  19382  odf1o1  19501  gex1  19520  sylow2alem1  19546  sylow2alem2  19547  lsm01  19600  lsm02  19601  lsmdisj  19610  lsmdisj2  19611  prmcyg  19823  gsumzadd  19851  gsumconst  19863  gsumdifsnd  19890  gsumpt  19891  gsumxp  19905  dmdprdd  19930  dprdfadd  19951  dprdres  19959  dprdz  19961  dprdsn  19967  dprddisj2  19970  dprd2da  19973  dprd2d2  19975  dmdprdsplit2lem  19976  dpjcntz  19983  dpjdisj  19984  dpjlsm  19985  dpjidcl  19989  ablfacrp  19997  ablfac1eu  20004  pgpfac1lem1  20005  pgpfac1lem3a  20007  pgpfac1lem3  20008  pgpfac1lem5  20010  pgpfaclem2  20013  acsfn1p  20732  lsssn0  20899  lss0ss  20900  lsptpcl  20930  lspsnvsi  20955  lspun0  20962  pwssplit1  21011  lsmpr  21041  lsppr  21045  lspsntri  21049  lspsolvlem  21097  lspsolv  21098  lsppratlem1  21102  lsppratlem3  21104  lsppratlem4  21105  islbs3  21110  lbsextlem4  21116  rnglidl0  21184  rsp1  21192  lidlnz  21197  lidldvgen  21289  mulgrhm2  21433  zndvds  21504  psrlidm  21917  psrridm  21918  mplmonmul  21991  mdetdiaglem  22542  mdetrlin  22546  mdetrsca  22547  mdetrsca2  22548  mdetrlin2  22551  mdetunilem5  22560  mdetunilem9  22564  mdetmul  22567  en2top  22929  rest0  23113  ordtrest  23146  iscnp4  23207  cnconst2  23227  cnpdis  23237  ist1-2  23291  cnt1  23294  dishaus  23326  discmp  23342  cmpcld  23346  conncompid  23375  dis2ndc  23404  dislly  23441  dissnref  23472  comppfsc  23476  llycmpkgen2  23494  cmpkgen  23495  1stckgenlem  23497  1stckgen  23498  ptbasfi  23525  txdis  23576  txdis1cn  23579  txcmplem1  23585  xkohaus  23597  xkoptsub  23598  xkoinjcn  23631  snfbas  23810  trnei  23836  isufil2  23852  ufileu  23863  filufint  23864  uffixsn  23869  ufildom1  23870  flimopn  23919  hausflim  23925  flimcf  23926  flimclslem  23928  flimsncls  23930  cnpflf2  23944  cnpflf  23945  fclsneii  23961  fclsfnflim  23971  fcfnei  23979  flfcntr  23987  alexsubALTlem3  23993  alexsubALTlem4  23994  ptcmplem2  23997  cldsubg  24055  snclseqg  24060  qustgphaus  24067  tsmsgsum  24083  tsmsid  24084  tgptsmscld  24095  tsmsxplem1  24097  tsmsxplem2  24098  ust0  24164  ustuqtop1  24185  neipcfilu  24239  prdsdsf  24311  prdsxmetlem  24312  prdsmet  24314  imasdsf1olem  24317  xpsdsval  24325  prdsbl  24435  prdsxmslem2  24473  idnghm  24687  icccmplem2  24768  metnrmlem2  24805  ioombl  25522  volivth  25564  itg11  25648  i1fmulclem  25659  itg2mulclem  25703  itgsplitioo  25795  limcvallem  25828  limcdif  25833  ellimc2  25834  limcflf  25838  limcmpt2  25841  limcres  25843  cnplimc  25844  limccnp  25848  limccnp2  25849  limcco  25850  dvreslem  25866  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  dvcmulf  25904  dvef  25940  dvivth  25971  lhop2  25976  lhop  25977  ply1remlem  26126  fta1blem  26132  ig1peu  26136  ig1pdvds  26141  plyco0  26153  elply2  26157  plyf  26159  elplyr  26162  elplyd  26163  ply1term  26165  ply0  26169  plyeq0lem  26171  plyeq0  26172  plypf1  26173  plyaddlem  26176  plymullem  26177  dgrlem  26190  coef2  26192  coeidlem  26198  plyco  26202  coemulhi  26215  plycj  26239  plycjOLD  26241  vieta1  26276  taylf  26324  radcnv0  26381  abelth  26407  rlimcnp  26931  xrlimcnp  26934  amgm  26957  wilthlem2  27035  basellem7  27053  basellem9  27055  ppiprm  27117  chtprm  27119  musumsum  27158  muinv  27159  logexprlim  27192  perfectlem2  27197  dchrhash  27238  rpvmasum2  27479  sltssnb  27765  lesrec  27795  eqcuts3  27800  cofcutr  27920  cutlt  27928  cutmax  27930  cutmin  27931  cutminmax  27932  addsuniflem  27997  negsunif  28051  sltmuls1  28143  sltmuls2  28144  precsexlem11  28213  oncutlt  28260  n0fincut  28351  bdaypw2n0bndlem  28459  axlowdimlem7  29021  axlowdimlem10  29024  upgrex  29165  upgr1elem  29185  uvtxnm1nbgr  29477  umgr2v2e  29599  cyclnumvtx  29873  0oo  30864  sh0le  31515  disjiunel  32671  preimane  32748  fnpreimac  32749  fsuppinisegfi  32766  fprodeq02  32904  indsn  32945  s1f1  33025  gsumzresunsn  33145  gsumhashmul  33150  pmtrcnelor  33173  primefldgen1  33403  dvdsrspss  33468  elgrplsmsn  33471  lsmsnorb  33472  grplsm0l  33484  grplsmid  33485  0ringidl  33502  unitpidl1  33505  elrspunsn  33510  drngidl  33514  isprmidlc  33528  qsidomlem2  33534  ssdifidlprm  33539  mxidlprm  33551  mxidlirredi  33552  mxidlirred  33553  drngmxidl  33558  drngmxidlr  33559  qsdrngilem  33575  rsprprmprmidl  33603  rprmirredb  33613  1arithufdlem4  33628  mvrvalind  33703  mplmulmvr  33704  evlextv  33707  esplyfval0  33722  esplyind  33731  esplyindfv  33732  vietalem  33735  lsatdim  33774  drngdimgt0  33775  dimkerim  33784  evls1fldgencl  33827  algextdeglem1  33874  algextdeglem2  33875  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  rtelextdg2  33884  constrextdg2lem  33905  constrext2chnlem  33907  constrfiss  33908  qtopt1  33992  locfinref  33998  zarcls0  34025  zarmxt1  34037  zarcmplem  34038  ordtrestNEW  34078  esumsnf  34221  esum2dlem  34249  rossros  34337  oms0  34454  carsggect  34475  eulerpartlems  34517  eulerpartlemgc  34519  eulerpartlemgh  34535  eulerpartlemgs2  34537  plymulx0  34704  circlemeth  34797  hgt750lemb  34813  hgt750leme  34815  bnj1452  35208  pthhashvtx  35322  subfacp1lem1  35373  subfacp1lem5  35378  erdszelem4  35388  erdszelem8  35392  sconnpi1  35433  cvmscld  35467  cvmlift2lem6  35502  cvmlift2lem9  35505  cvmlift2lem11  35507  cvmlift2lem12  35508  mrsubvrs  35716  ellcsrspsn  35835  neibastop2lem  36554  topjoin  36559  fnejoin2  36563  weiunse  36662  pibt2  37622  lindsadd  37814  poimirlem3  37824  poimirlem9  37830  poimirlem28  37849  poimirlem32  37853  prdsbnd  37994  heiborlem8  38019  rrnequiv  38036  grpokerinj  38094  0idl  38226  prnc  38268  isfldidl  38269  lshpnel2N  39255  lsatfixedN  39279  lfl0f  39339  lkrlsp3  39374  elpaddatriN  40073  elpaddat  40074  elpadd2at  40076  pmodlem1  40116  osumcllem1N  40226  osumcllem2N  40227  osumcllem9N  40234  osumcllem10N  40235  pexmidlem6N  40245  pexmidlem7N  40246  dibss  41439  dochocsn  41651  dochsncom  41652  dochnel  41663  dihprrnlem1N  41694  dihprrnlem2  41695  djhlsmat  41697  dihsmsprn  41700  dvh4dimlem  41713  dvhdimlem  41714  dochsnnz  41720  dochsatshp  41721  dochsnshp  41723  dochexmid  41738  dochsnkr  41742  dochsnkr2cl  41744  dochfl1  41746  lcfl7lem  41769  lcfl6  41770  lcfl8  41772  lcfl9a  41775  lclkrlem2a  41777  lclkrlem2c  41779  lclkrlem2d  41780  lclkrlem2e  41781  lclkrlem2j  41786  lclkrlem2o  41791  lclkrlem2p  41792  lclkrlem2s  41795  lclkrlem2v  41798  lcfrlem14  41826  lcfrlem18  41830  lcfrlem19  41831  lcfrlem20  41832  lcfrlem23  41835  lcfrlem25  41837  lcdlkreqN  41892  mapdval4N  41902  mapdsn  41911  mapdhvmap  42039  hdmaprnlem4tN  42122  hdmapinvlem1  42188  hdmapinvlem2  42189  hdmapinvlem3  42190  hdmapinvlem4  42191  hdmapglem5  42192  hgmapvvlem3  42195  hdmapglem7a  42197  hdmapglem7b  42198  hdmapglem7  42199  hdmapoc  42201  aks6d1c5lem3  42401  deg1gprod  42404  sticksstones9  42418  sticksstones11  42420  rhmqusspan  42449  evlsbagval  42822  selvvvval  42838  0prjspnrel  42880  elrfi  42946  cmpfiiin  42949  mzpcompact2lem  43003  dfac11  43314  pwssplit4  43341  rngunsnply  43421  flcidc  43422  proot1mul  43446  iocinico  43464  cantnfresb  43576  iunrelexp0  43953  frege81d  43998  k0004lem3  44400  mnuunid  44528  binomcxplemnn0  44600  islptre  45875  limciccioolb  45877  limcicciooub  45891  limcresiooub  45896  limcresioolb  45897  ioccncflimc  46139  icccncfext  46141  icocncflimc  46143  cncfiooicc  46148  dvnprodlem2  46201  dirkercncflem2  46358  dirkercncflem3  46359  fourierdlem48  46408  fourierdlem49  46409  fourierdlem79  46439  fourierdlem101  46461  sge0sup  46645  hoidmvlelem2  46850  hoiqssbl  46879  hspmbllem1  46880  hspmbllem2  46881  ovnovollem1  46910  fsumsplitsndif  47629  imaelsetpreimafv  47651  perfectALTVlem2  47978  stgrclnbgr0  48221  isubgr3stgrlem3  48224  1hegrlfgr  48388  gsumdifsndf  48437  sepfsepc  49183  discsubc  49319  iinfconstbas  49321