Theorem snssd 4760

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903  {csn 4577

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-ss 3920  df-sn 4578

This theorem is referenced by:  intidg  5400  sofld  6136  fsnex  7220  fr3nr  7708  resf1extb  7867  resf1ext2b  7868  frrlem13  8231  oeeui  8520  naddunif  8611  naddasslem1  8612  naddasslem2  8613  ecinxp  8719  ralxpmap  8823  xpdom3  8992  domunsn  9044  mapdom3  9066  isinf  9154  ac6sfi  9173  pwfilem  9207  finsschain  9249  ssfii  9309  marypha1lem  9323  unxpwdom2  9480  en2other2  9903  fseqenlem1  9918  axdc3lem4  10347  axdc4lem  10349  ttukeylem7  10409  fpwwe2lem12  10536  canthwe  10545  canthp1lem1  10546  wuncval2  10641  un0addcl  12417  un0mulcl  12418  ssfzunsnext  13472  fseq1p1m1  13501  hashbclem  14359  hashf1lem1  14362  fsumsplit1  15652  fsumge1  15704  incexclem  15743  isumltss  15755  fprodsplit1f  15897  rpnnen2lem11  16133  bitsinv1  16353  lcmfunsnlem2  16551  lcmfass  16557  phicl2  16679  vdwlem1  16893  vdwlem8  16900  vdwlem12  16904  vdwlem13  16905  0ram  16932  ramub1lem1  16938  ramub1lem2  16939  ramcl  16941  imasaddfnlem  17432  imasaddflem  17434  imasvscafn  17441  imasvscaf  17443  mrieqvlemd  17535  mreexmrid  17549  mreexexlem4d  17553  acsfiindd  18459  acsmapd  18460  gsumress  18556  0subm  18691  gsumvallem2  18708  0subgOLD  19031  trivsubgd  19032  trivsubgsnd  19033  trivnsgd  19051  cycsubg2cl  19090  kerf1ghm  19126  pmtrprfv  19332  odf1o1  19451  gex1  19470  sylow2alem1  19496  sylow2alem2  19497  lsm01  19550  lsm02  19551  lsmdisj  19560  lsmdisj2  19561  prmcyg  19773  gsumzadd  19801  gsumconst  19813  gsumdifsnd  19840  gsumpt  19841  gsumxp  19855  dmdprdd  19880  dprdfadd  19901  dprdres  19909  dprdz  19911  dprdsn  19917  dprddisj2  19920  dprd2da  19923  dprd2d2  19925  dmdprdsplit2lem  19926  dpjcntz  19933  dpjdisj  19934  dpjlsm  19935  dpjidcl  19939  ablfacrp  19947  ablfac1eu  19954  pgpfac1lem1  19955  pgpfac1lem3a  19957  pgpfac1lem3  19958  pgpfac1lem5  19960  pgpfaclem2  19963  acsfn1p  20684  lsssn0  20851  lss0ss  20852  lsptpcl  20882  lspsnvsi  20907  lspun0  20914  pwssplit1  20963  lsmpr  20993  lsppr  20997  lspsntri  21001  lspsolvlem  21049  lspsolv  21050  lsppratlem1  21054  lsppratlem3  21056  lsppratlem4  21057  islbs3  21062  lbsextlem4  21068  rnglidl0  21136  rsp1  21144  lidlnz  21149  lidldvgen  21241  mulgrhm2  21385  zndvds  21456  psrlidm  21869  psrridm  21870  mplmonmul  21941  mdetdiaglem  22483  mdetrlin  22487  mdetrsca  22488  mdetrsca2  22489  mdetrlin2  22492  mdetunilem5  22501  mdetunilem9  22505  mdetmul  22508  en2top  22870  rest0  23054  ordtrest  23087  iscnp4  23148  cnconst2  23168  cnpdis  23178  ist1-2  23232  cnt1  23235  dishaus  23267  discmp  23283  cmpcld  23287  conncompid  23316  dis2ndc  23345  dislly  23382  dissnref  23413  comppfsc  23417  llycmpkgen2  23435  cmpkgen  23436  1stckgenlem  23438  1stckgen  23439  ptbasfi  23466  txdis  23517  txdis1cn  23520  txcmplem1  23526  xkohaus  23538  xkoptsub  23539  xkoinjcn  23572  snfbas  23751  trnei  23777  isufil2  23793  ufileu  23804  filufint  23805  uffixsn  23810  ufildom1  23811  flimopn  23860  hausflim  23866  flimcf  23867  flimclslem  23869  flimsncls  23871  cnpflf2  23885  cnpflf  23886  fclsneii  23902  fclsfnflim  23912  fcfnei  23920  flfcntr  23928  alexsubALTlem3  23934  alexsubALTlem4  23935  ptcmplem2  23938  cldsubg  23996  snclseqg  24001  qustgphaus  24008  tsmsgsum  24024  tsmsid  24025  tgptsmscld  24036  tsmsxplem1  24038  tsmsxplem2  24039  ust0  24105  ustuqtop1  24127  neipcfilu  24181  prdsdsf  24253  prdsxmetlem  24254  prdsmet  24256  imasdsf1olem  24259  xpsdsval  24267  prdsbl  24377  prdsxmslem2  24415  idnghm  24629  icccmplem2  24710  metnrmlem2  24747  ioombl  25464  volivth  25506  itg11  25590  i1fmulclem  25601  itg2mulclem  25645  itgsplitioo  25737  limcvallem  25770  limcdif  25775  ellimc2  25776  limcflf  25780  limcmpt2  25783  limcres  25785  cnplimc  25786  limccnp  25790  limccnp2  25791  limcco  25792  dvreslem  25808  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  dvcmulf  25846  dvef  25882  dvivth  25913  lhop2  25918  lhop  25919  ply1remlem  26068  fta1blem  26074  ig1peu  26078  ig1pdvds  26083  plyco0  26095  elply2  26099  plyf  26101  elplyr  26104  elplyd  26105  ply1term  26107  ply0  26111  plyeq0lem  26113  plyeq0  26114  plypf1  26115  plyaddlem  26118  plymullem  26119  dgrlem  26132  coef2  26134  coeidlem  26140  plyco  26144  coemulhi  26157  plycj  26181  plycjOLD  26183  vieta1  26218  taylf  26266  radcnv0  26323  abelth  26349  rlimcnp  26873  xrlimcnp  26876  amgm  26899  wilthlem2  26977  basellem7  26995  basellem9  26997  ppiprm  27059  chtprm  27061  musumsum  27100  muinv  27101  logexprlim  27134  perfectlem2  27139  dchrhash  27180  rpvmasum2  27421  ssltsn  27703  slerec  27730  eqscut3  27735  cofcutr  27837  cutlt  27845  cutmax  27847  cutmin  27848  addsuniflem  27913  negsunif  27966  ssltmul1  28055  ssltmul2  28056  precsexlem11  28124  onscutlt  28170  n0sfincut  28251  0reno  28366  axlowdimlem7  28893  axlowdimlem10  28896  upgrex  29037  upgr1elem  29057  uvtxnm1nbgr  29349  umgr2v2e  29471  cyclnumvtx  29745  0oo  30733  sh0le  31384  disjiunel  32540  preimane  32613  fnpreimac  32614  fsuppinisegfi  32629  fprodeq02  32768  s1f1  32884  gsumzresunsn  33009  gsumhashmul  33014  pmtrcnelor  33033  primefldgen1  33260  dvdsrspss  33324  elgrplsmsn  33327  lsmsnorb  33328  grplsm0l  33340  grplsmid  33341  0ringidl  33358  unitpidl1  33361  elrspunsn  33366  drngidl  33370  isprmidlc  33384  qsidomlem2  33390  ssdifidlprm  33395  mxidlprm  33407  mxidlirredi  33408  mxidlirred  33409  drngmxidl  33414  drngmxidlr  33415  qsdrngilem  33431  rsprprmprmidl  33459  rprmirredb  33469  1arithufdlem4  33484  lsatdim  33584  drngdimgt0  33585  dimkerim  33594  evls1fldgencl  33637  algextdeglem1  33684  algextdeglem2  33685  algextdeglem3  33686  algextdeglem4  33687  algextdeglem5  33688  rtelextdg2  33694  constrextdg2lem  33715  constrext2chnlem  33717  constrfiss  33718  qtopt1  33802  locfinref  33808  zarcls0  33835  zarmxt1  33847  zarcmplem  33848  ordtrestNEW  33888  esumsnf  34031  esum2dlem  34059  rossros  34147  oms0  34265  carsggect  34286  eulerpartlems  34328  eulerpartlemgc  34330  eulerpartlemgh  34346  eulerpartlemgs2  34348  plymulx0  34515  circlemeth  34608  hgt750lemb  34624  hgt750leme  34626  bnj1452  35019  pthhashvtx  35105  subfacp1lem1  35156  subfacp1lem5  35161  erdszelem4  35171  erdszelem8  35175  sconnpi1  35216  cvmscld  35250  cvmlift2lem6  35285  cvmlift2lem9  35288  cvmlift2lem11  35290  cvmlift2lem12  35291  mrsubvrs  35499  ellcsrspsn  35618  neibastop2lem  36338  topjoin  36343  fnejoin2  36347  weiunse  36446  pibt2  37395  lindsadd  37597  poimirlem3  37607  poimirlem9  37613  poimirlem28  37632  poimirlem32  37636  prdsbnd  37777  heiborlem8  37802  rrnequiv  37819  grpokerinj  37877  0idl  38009  prnc  38051  isfldidl  38052  lshpnel2N  38968  lsatfixedN  38992  lfl0f  39052  lkrlsp3  39087  elpaddatriN  39786  elpaddat  39787  elpadd2at  39789  pmodlem1  39829  osumcllem1N  39939  osumcllem2N  39940  osumcllem9N  39947  osumcllem10N  39948  pexmidlem6N  39958  pexmidlem7N  39959  dibss  41152  dochocsn  41364  dochsncom  41365  dochnel  41376  dihprrnlem1N  41407  dihprrnlem2  41408  djhlsmat  41410  dihsmsprn  41413  dvh4dimlem  41426  dvhdimlem  41427  dochsnnz  41433  dochsatshp  41434  dochsnshp  41436  dochexmid  41451  dochsnkr  41455  dochsnkr2cl  41457  dochfl1  41459  lcfl7lem  41482  lcfl6  41483  lcfl8  41485  lcfl9a  41488  lclkrlem2a  41490  lclkrlem2c  41492  lclkrlem2d  41493  lclkrlem2e  41494  lclkrlem2j  41499  lclkrlem2o  41504  lclkrlem2p  41505  lclkrlem2s  41508  lclkrlem2v  41511  lcfrlem14  41539  lcfrlem18  41543  lcfrlem19  41544  lcfrlem20  41545  lcfrlem23  41548  lcfrlem25  41550  lcdlkreqN  41605  mapdval4N  41615  mapdsn  41624  mapdhvmap  41752  hdmaprnlem4tN  41835  hdmapinvlem1  41901  hdmapinvlem2  41902  hdmapinvlem3  41903  hdmapinvlem4  41904  hdmapglem5  41905  hgmapvvlem3  41908  hdmapglem7a  41910  hdmapglem7b  41911  hdmapglem7  41912  hdmapoc  41914  aks6d1c5lem3  42114  deg1gprod  42117  sticksstones9  42131  sticksstones11  42133  rhmqusspan  42162  evlsbagval  42543  selvvvval  42562  0prjspnrel  42604  elrfi  42671  cmpfiiin  42674  mzpcompact2lem  42728  dfac11  43039  pwssplit4  43066  rngunsnply  43146  flcidc  43147  proot1mul  43171  iocinico  43189  cantnfresb  43301  iunrelexp0  43679  frege81d  43724  k0004lem3  44126  mnuunid  44254  binomcxplemnn0  44326  islptre  45604  limciccioolb  45606  limcicciooub  45622  limcresiooub  45627  limcresioolb  45628  ioccncflimc  45870  icccncfext  45872  icocncflimc  45874  cncfiooicc  45879  dvnprodlem2  45932  dirkercncflem2  46089  dirkercncflem3  46090  fourierdlem48  46139  fourierdlem49  46140  fourierdlem79  46170  fourierdlem101  46192  sge0sup  46376  hoidmvlelem2  46581  hoiqssbl  46610  hspmbllem1  46611  hspmbllem2  46612  ovnovollem1  46641  fsumsplitsndif  47361  imaelsetpreimafv  47383  perfectALTVlem2  47710  stgrclnbgr0  47953  isubgr3stgrlem3  47956  1hegrlfgr  48120  gsumdifsndf  48169  sepfsepc  48916  discsubc  49053  iinfconstbas  49055