Theorem snssd 4763

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3899  {csn 4578

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-ss 3916  df-sn 4579

This theorem is referenced by:  intidg  5403  sofld  6143  fsnex  7227  fr3nr  7715  resf1extb  7874  resf1ext2b  7875  frrlem13  8238  oeeui  8528  naddunif  8619  naddasslem1  8620  naddasslem2  8621  ecinxp  8727  ralxpmap  8832  xpdom3  9001  domunsn  9053  mapdom3  9075  isinf  9163  ac6sfi  9182  pwfilem  9216  finsschain  9257  ssfii  9320  marypha1lem  9334  unxpwdom2  9491  en2other2  9917  fseqenlem1  9932  axdc3lem4  10361  axdc4lem  10363  ttukeylem7  10423  fpwwe2lem12  10551  canthwe  10560  canthp1lem1  10561  wuncval2  10656  un0addcl  12432  un0mulcl  12433  ssfzunsnext  13483  fseq1p1m1  13512  hashbclem  14373  hashf1lem1  14376  fsumsplit1  15666  fsumge1  15718  incexclem  15757  isumltss  15769  fprodsplit1f  15911  rpnnen2lem11  16147  bitsinv1  16367  lcmfunsnlem2  16565  lcmfass  16571  phicl2  16693  vdwlem1  16907  vdwlem8  16914  vdwlem12  16918  vdwlem13  16919  0ram  16946  ramub1lem1  16952  ramub1lem2  16953  ramcl  16955  imasaddfnlem  17447  imasaddflem  17449  imasvscafn  17456  imasvscaf  17458  mrieqvlemd  17550  mreexmrid  17564  mreexexlem4d  17568  acsfiindd  18474  acsmapd  18475  chnccat  18547  gsumress  18605  0subm  18740  gsumvallem2  18757  trivsubgd  19080  trivsubgsnd  19081  trivnsgd  19099  cycsubg2cl  19138  kerf1ghm  19174  pmtrprfv  19380  odf1o1  19499  gex1  19518  sylow2alem1  19544  sylow2alem2  19545  lsm01  19598  lsm02  19599  lsmdisj  19608  lsmdisj2  19609  prmcyg  19821  gsumzadd  19849  gsumconst  19861  gsumdifsnd  19888  gsumpt  19889  gsumxp  19903  dmdprdd  19928  dprdfadd  19949  dprdres  19957  dprdz  19959  dprdsn  19965  dprddisj2  19968  dprd2da  19971  dprd2d2  19973  dmdprdsplit2lem  19974  dpjcntz  19981  dpjdisj  19982  dpjlsm  19983  dpjidcl  19987  ablfacrp  19995  ablfac1eu  20002  pgpfac1lem1  20003  pgpfac1lem3a  20005  pgpfac1lem3  20006  pgpfac1lem5  20008  pgpfaclem2  20011  acsfn1p  20730  lsssn0  20897  lss0ss  20898  lsptpcl  20928  lspsnvsi  20953  lspun0  20960  pwssplit1  21009  lsmpr  21039  lsppr  21043  lspsntri  21047  lspsolvlem  21095  lspsolv  21096  lsppratlem1  21100  lsppratlem3  21102  lsppratlem4  21103  islbs3  21108  lbsextlem4  21114  rnglidl0  21182  rsp1  21190  lidlnz  21195  lidldvgen  21287  mulgrhm2  21431  zndvds  21502  psrlidm  21915  psrridm  21916  mplmonmul  21989  mdetdiaglem  22540  mdetrlin  22544  mdetrsca  22545  mdetrsca2  22546  mdetrlin2  22549  mdetunilem5  22558  mdetunilem9  22562  mdetmul  22565  en2top  22927  rest0  23111  ordtrest  23144  iscnp4  23205  cnconst2  23225  cnpdis  23235  ist1-2  23289  cnt1  23292  dishaus  23324  discmp  23340  cmpcld  23344  conncompid  23373  dis2ndc  23402  dislly  23439  dissnref  23470  comppfsc  23474  llycmpkgen2  23492  cmpkgen  23493  1stckgenlem  23495  1stckgen  23496  ptbasfi  23523  txdis  23574  txdis1cn  23577  txcmplem1  23583  xkohaus  23595  xkoptsub  23596  xkoinjcn  23629  snfbas  23808  trnei  23834  isufil2  23850  ufileu  23861  filufint  23862  uffixsn  23867  ufildom1  23868  flimopn  23917  hausflim  23923  flimcf  23924  flimclslem  23926  flimsncls  23928  cnpflf2  23942  cnpflf  23943  fclsneii  23959  fclsfnflim  23969  fcfnei  23977  flfcntr  23985  alexsubALTlem3  23991  alexsubALTlem4  23992  ptcmplem2  23995  cldsubg  24053  snclseqg  24058  qustgphaus  24065  tsmsgsum  24081  tsmsid  24082  tgptsmscld  24093  tsmsxplem1  24095  tsmsxplem2  24096  ust0  24162  ustuqtop1  24183  neipcfilu  24237  prdsdsf  24309  prdsxmetlem  24310  prdsmet  24312  imasdsf1olem  24315  xpsdsval  24323  prdsbl  24433  prdsxmslem2  24471  idnghm  24685  icccmplem2  24766  metnrmlem2  24803  ioombl  25520  volivth  25562  itg11  25646  i1fmulclem  25657  itg2mulclem  25701  itgsplitioo  25793  limcvallem  25826  limcdif  25831  ellimc2  25832  limcflf  25836  limcmpt2  25839  limcres  25841  cnplimc  25842  limccnp  25846  limccnp2  25847  limcco  25848  dvreslem  25864  dvaddbr  25894  dvmulbr  25895  dvmulbrOLD  25896  dvcmulf  25902  dvef  25938  dvivth  25969  lhop2  25974  lhop  25975  ply1remlem  26124  fta1blem  26130  ig1peu  26134  ig1pdvds  26139  plyco0  26151  elply2  26155  plyf  26157  elplyr  26160  elplyd  26161  ply1term  26163  ply0  26167  plyeq0lem  26169  plyeq0  26170  plypf1  26171  plyaddlem  26174  plymullem  26175  dgrlem  26188  coef2  26190  coeidlem  26196  plyco  26200  coemulhi  26213  plycj  26237  plycjOLD  26239  vieta1  26274  taylf  26322  radcnv0  26379  abelth  26405  rlimcnp  26929  xrlimcnp  26932  amgm  26955  wilthlem2  27033  basellem7  27051  basellem9  27053  ppiprm  27115  chtprm  27117  musumsum  27156  muinv  27157  logexprlim  27190  perfectlem2  27195  dchrhash  27236  rpvmasum2  27477  ssltsnb  27759  slerec  27787  eqscut3  27792  cofcutr  27895  cutlt  27903  cutmax  27905  cutmin  27906  addsuniflem  27971  negsunif  28024  ssltmul1  28116  ssltmul2  28117  precsexlem11  28185  onscutlt  28232  n0sfincut  28315  bdaypw2n0s  28420  axlowdimlem7  28970  axlowdimlem10  28973  upgrex  29114  upgr1elem  29134  uvtxnm1nbgr  29426  umgr2v2e  29548  cyclnumvtx  29822  0oo  30813  sh0le  31464  disjiunel  32620  preimane  32697  fnpreimac  32698  fsuppinisegfi  32715  fprodeq02  32853  indsn  32894  s1f1  32974  gsumzresunsn  33094  gsumhashmul  33099  pmtrcnelor  33122  primefldgen1  33352  dvdsrspss  33417  elgrplsmsn  33420  lsmsnorb  33421  grplsm0l  33433  grplsmid  33434  0ringidl  33451  unitpidl1  33454  elrspunsn  33459  drngidl  33463  isprmidlc  33477  qsidomlem2  33483  ssdifidlprm  33488  mxidlprm  33500  mxidlirredi  33501  mxidlirred  33502  drngmxidl  33507  drngmxidlr  33508  qsdrngilem  33524  rsprprmprmidl  33552  rprmirredb  33562  1arithufdlem4  33577  mvrvalind  33652  mplmulmvr  33653  evlextv  33656  esplyfval0  33671  esplyind  33680  esplyindfv  33681  vietalem  33684  lsatdim  33723  drngdimgt0  33724  dimkerim  33733  evls1fldgencl  33776  algextdeglem1  33823  algextdeglem2  33824  algextdeglem3  33825  algextdeglem4  33826  algextdeglem5  33827  rtelextdg2  33833  constrextdg2lem  33854  constrext2chnlem  33856  constrfiss  33857  qtopt1  33941  locfinref  33947  zarcls0  33974  zarmxt1  33986  zarcmplem  33987  ordtrestNEW  34027  esumsnf  34170  esum2dlem  34198  rossros  34286  oms0  34403  carsggect  34424  eulerpartlems  34466  eulerpartlemgc  34468  eulerpartlemgh  34484  eulerpartlemgs2  34486  plymulx0  34653  circlemeth  34746  hgt750lemb  34762  hgt750leme  34764  bnj1452  35157  pthhashvtx  35271  subfacp1lem1  35322  subfacp1lem5  35327  erdszelem4  35337  erdszelem8  35341  sconnpi1  35382  cvmscld  35416  cvmlift2lem6  35451  cvmlift2lem9  35454  cvmlift2lem11  35456  cvmlift2lem12  35457  mrsubvrs  35665  ellcsrspsn  35784  neibastop2lem  36503  topjoin  36508  fnejoin2  36512  weiunse  36611  pibt2  37561  lindsadd  37753  poimirlem3  37763  poimirlem9  37769  poimirlem28  37788  poimirlem32  37792  prdsbnd  37933  heiborlem8  37958  rrnequiv  37975  grpokerinj  38033  0idl  38165  prnc  38207  isfldidl  38208  lshpnel2N  39184  lsatfixedN  39208  lfl0f  39268  lkrlsp3  39303  elpaddatriN  40002  elpaddat  40003  elpadd2at  40005  pmodlem1  40045  osumcllem1N  40155  osumcllem2N  40156  osumcllem9N  40163  osumcllem10N  40164  pexmidlem6N  40174  pexmidlem7N  40175  dibss  41368  dochocsn  41580  dochsncom  41581  dochnel  41592  dihprrnlem1N  41623  dihprrnlem2  41624  djhlsmat  41626  dihsmsprn  41629  dvh4dimlem  41642  dvhdimlem  41643  dochsnnz  41649  dochsatshp  41650  dochsnshp  41652  dochexmid  41667  dochsnkr  41671  dochsnkr2cl  41673  dochfl1  41675  lcfl7lem  41698  lcfl6  41699  lcfl8  41701  lcfl9a  41704  lclkrlem2a  41706  lclkrlem2c  41708  lclkrlem2d  41709  lclkrlem2e  41710  lclkrlem2j  41715  lclkrlem2o  41720  lclkrlem2p  41721  lclkrlem2s  41724  lclkrlem2v  41727  lcfrlem14  41755  lcfrlem18  41759  lcfrlem19  41760  lcfrlem20  41761  lcfrlem23  41764  lcfrlem25  41766  lcdlkreqN  41821  mapdval4N  41831  mapdsn  41840  mapdhvmap  41968  hdmaprnlem4tN  42051  hdmapinvlem1  42117  hdmapinvlem2  42118  hdmapinvlem3  42119  hdmapinvlem4  42120  hdmapglem5  42121  hgmapvvlem3  42124  hdmapglem7a  42126  hdmapglem7b  42127  hdmapglem7  42128  hdmapoc  42130  aks6d1c5lem3  42330  deg1gprod  42333  sticksstones9  42347  sticksstones11  42349  rhmqusspan  42378  evlsbagval  42754  selvvvval  42770  0prjspnrel  42812  elrfi  42878  cmpfiiin  42881  mzpcompact2lem  42935  dfac11  43246  pwssplit4  43273  rngunsnply  43353  flcidc  43354  proot1mul  43378  iocinico  43396  cantnfresb  43508  iunrelexp0  43885  frege81d  43930  k0004lem3  44332  mnuunid  44460  binomcxplemnn0  44532  islptre  45807  limciccioolb  45809  limcicciooub  45823  limcresiooub  45828  limcresioolb  45829  ioccncflimc  46071  icccncfext  46073  icocncflimc  46075  cncfiooicc  46080  dvnprodlem2  46133  dirkercncflem2  46290  dirkercncflem3  46291  fourierdlem48  46340  fourierdlem49  46341  fourierdlem79  46371  fourierdlem101  46393  sge0sup  46577  hoidmvlelem2  46782  hoiqssbl  46811  hspmbllem1  46812  hspmbllem2  46813  ovnovollem1  46842  fsumsplitsndif  47561  imaelsetpreimafv  47583  perfectALTVlem2  47910  stgrclnbgr0  48153  isubgr3stgrlem3  48156  1hegrlfgr  48320  gsumdifsndf  48369  sepfsepc  49115  discsubc  49251  iinfconstbas  49253