Theorem snssd 4767

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3903  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-ss 3920  df-sn 4583

This theorem is referenced by:  intidg  5412  sofld  6153  fsnex  7239  fr3nr  7727  resf1extb  7886  resf1ext2b  7887  frrlem13  8250  oeeui  8540  naddunif  8631  naddasslem1  8632  naddasslem2  8633  ecinxp  8741  ralxpmap  8846  xpdom3  9015  domunsn  9067  mapdom3  9089  isinf  9177  ac6sfi  9196  pwfilem  9230  finsschain  9271  ssfii  9334  marypha1lem  9348  unxpwdom2  9505  en2other2  9931  fseqenlem1  9946  axdc3lem4  10375  axdc4lem  10377  ttukeylem7  10437  fpwwe2lem12  10565  canthwe  10574  canthp1lem1  10575  wuncval2  10670  un0addcl  12446  un0mulcl  12447  ssfzunsnext  13497  fseq1p1m1  13526  hashbclem  14387  hashf1lem1  14390  fsumsplit1  15680  fsumge1  15732  incexclem  15771  isumltss  15783  fprodsplit1f  15925  rpnnen2lem11  16161  bitsinv1  16381  lcmfunsnlem2  16579  lcmfass  16585  phicl2  16707  vdwlem1  16921  vdwlem8  16928  vdwlem12  16932  vdwlem13  16933  0ram  16960  ramub1lem1  16966  ramub1lem2  16967  ramcl  16969  imasaddfnlem  17461  imasaddflem  17463  imasvscafn  17470  imasvscaf  17472  mrieqvlemd  17564  mreexmrid  17578  mreexexlem4d  17582  acsfiindd  18488  acsmapd  18489  chnccat  18561  gsumress  18619  0subm  18754  gsumvallem2  18771  trivsubgd  19094  trivsubgsnd  19095  trivnsgd  19113  cycsubg2cl  19152  kerf1ghm  19188  pmtrprfv  19394  odf1o1  19513  gex1  19532  sylow2alem1  19558  sylow2alem2  19559  lsm01  19612  lsm02  19613  lsmdisj  19622  lsmdisj2  19623  prmcyg  19835  gsumzadd  19863  gsumconst  19875  gsumdifsnd  19902  gsumpt  19903  gsumxp  19917  dmdprdd  19942  dprdfadd  19963  dprdres  19971  dprdz  19973  dprdsn  19979  dprddisj2  19982  dprd2da  19985  dprd2d2  19987  dmdprdsplit2lem  19988  dpjcntz  19995  dpjdisj  19996  dpjlsm  19997  dpjidcl  20001  ablfacrp  20009  ablfac1eu  20016  pgpfac1lem1  20017  pgpfac1lem3a  20019  pgpfac1lem3  20020  pgpfac1lem5  20022  pgpfaclem2  20025  acsfn1p  20744  lsssn0  20911  lss0ss  20912  lsptpcl  20942  lspsnvsi  20967  lspun0  20974  pwssplit1  21023  lsmpr  21053  lsppr  21057  lspsntri  21061  lspsolvlem  21109  lspsolv  21110  lsppratlem1  21114  lsppratlem3  21116  lsppratlem4  21117  islbs3  21122  lbsextlem4  21128  rnglidl0  21196  rsp1  21204  lidlnz  21209  lidldvgen  21301  mulgrhm2  21445  zndvds  21516  psrlidm  21929  psrridm  21930  mplmonmul  22003  mdetdiaglem  22554  mdetrlin  22558  mdetrsca  22559  mdetrsca2  22560  mdetrlin2  22563  mdetunilem5  22572  mdetunilem9  22576  mdetmul  22579  en2top  22941  rest0  23125  ordtrest  23158  iscnp4  23219  cnconst2  23239  cnpdis  23249  ist1-2  23303  cnt1  23306  dishaus  23338  discmp  23354  cmpcld  23358  conncompid  23387  dis2ndc  23416  dislly  23453  dissnref  23484  comppfsc  23488  llycmpkgen2  23506  cmpkgen  23507  1stckgenlem  23509  1stckgen  23510  ptbasfi  23537  txdis  23588  txdis1cn  23591  txcmplem1  23597  xkohaus  23609  xkoptsub  23610  xkoinjcn  23643  snfbas  23822  trnei  23848  isufil2  23864  ufileu  23875  filufint  23876  uffixsn  23881  ufildom1  23882  flimopn  23931  hausflim  23937  flimcf  23938  flimclslem  23940  flimsncls  23942  cnpflf2  23956  cnpflf  23957  fclsneii  23973  fclsfnflim  23983  fcfnei  23991  flfcntr  23999  alexsubALTlem3  24005  alexsubALTlem4  24006  ptcmplem2  24009  cldsubg  24067  snclseqg  24072  qustgphaus  24079  tsmsgsum  24095  tsmsid  24096  tgptsmscld  24107  tsmsxplem1  24109  tsmsxplem2  24110  ust0  24176  ustuqtop1  24197  neipcfilu  24251  prdsdsf  24323  prdsxmetlem  24324  prdsmet  24326  imasdsf1olem  24329  xpsdsval  24337  prdsbl  24447  prdsxmslem2  24485  idnghm  24699  icccmplem2  24780  metnrmlem2  24817  ioombl  25534  volivth  25576  itg11  25660  i1fmulclem  25671  itg2mulclem  25715  itgsplitioo  25807  limcvallem  25840  limcdif  25845  ellimc2  25846  limcflf  25850  limcmpt2  25853  limcres  25855  cnplimc  25856  limccnp  25860  limccnp2  25861  limcco  25862  dvreslem  25878  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvcmulf  25916  dvef  25952  dvivth  25983  lhop2  25988  lhop  25989  ply1remlem  26138  fta1blem  26144  ig1peu  26148  ig1pdvds  26153  plyco0  26165  elply2  26169  plyf  26171  elplyr  26174  elplyd  26175  ply1term  26177  ply0  26181  plyeq0lem  26183  plyeq0  26184  plypf1  26185  plyaddlem  26188  plymullem  26189  dgrlem  26202  coef2  26204  coeidlem  26210  plyco  26214  coemulhi  26227  plycj  26251  plycjOLD  26253  vieta1  26288  taylf  26336  radcnv0  26393  abelth  26419  rlimcnp  26943  xrlimcnp  26946  amgm  26969  wilthlem2  27047  basellem7  27065  basellem9  27067  ppiprm  27129  chtprm  27131  musumsum  27170  muinv  27171  logexprlim  27204  perfectlem2  27209  dchrhash  27250  rpvmasum2  27491  sltssnb  27777  lesrec  27807  eqcuts3  27812  cofcutr  27932  cutlt  27940  cutmax  27942  cutmin  27943  cutminmax  27944  addsuniflem  28009  negsunif  28063  sltmuls1  28155  sltmuls2  28156  precsexlem11  28225  oncutlt  28272  n0fincut  28363  bdaypw2n0bndlem  28471  axlowdimlem7  29033  axlowdimlem10  29036  upgrex  29177  upgr1elem  29197  uvtxnm1nbgr  29489  umgr2v2e  29611  cyclnumvtx  29885  0oo  30877  sh0le  31528  disjiunel  32683  preimane  32759  fnpreimac  32760  fsuppinisegfi  32777  fprodeq02  32915  indsn  32956  s1f1  33036  gsumzresunsn  33156  gsumhashmul  33161  pmtrcnelor  33185  primefldgen1  33415  dvdsrspss  33480  elgrplsmsn  33483  lsmsnorb  33484  grplsm0l  33496  grplsmid  33497  0ringidl  33514  unitpidl1  33517  elrspunsn  33522  drngidl  33526  isprmidlc  33540  qsidomlem2  33546  ssdifidlprm  33551  mxidlprm  33563  mxidlirredi  33564  mxidlirred  33565  drngmxidl  33570  drngmxidlr  33571  qsdrngilem  33587  rsprprmprmidl  33615  rprmirredb  33625  1arithufdlem4  33640  mvrvalind  33715  mplmulmvr  33716  evlextv  33719  psrmonmul  33727  esplyfval0  33741  esplyfvaln  33751  esplyind  33752  esplyindfv  33753  vietalem  33756  lsatdim  33795  drngdimgt0  33796  dimkerim  33805  evls1fldgencl  33848  algextdeglem1  33895  algextdeglem2  33896  algextdeglem3  33897  algextdeglem4  33898  algextdeglem5  33899  rtelextdg2  33905  constrextdg2lem  33926  constrext2chnlem  33928  constrfiss  33929  qtopt1  34013  locfinref  34019  zarcls0  34046  zarmxt1  34058  zarcmplem  34059  ordtrestNEW  34099  esumsnf  34242  esum2dlem  34270  rossros  34358  oms0  34475  carsggect  34496  eulerpartlems  34538  eulerpartlemgc  34540  eulerpartlemgh  34556  eulerpartlemgs2  34558  plymulx0  34725  circlemeth  34818  hgt750lemb  34834  hgt750leme  34836  bnj1452  35228  pthhashvtx  35344  subfacp1lem1  35395  subfacp1lem5  35400  erdszelem4  35410  erdszelem8  35414  sconnpi1  35455  cvmscld  35489  cvmlift2lem6  35524  cvmlift2lem9  35527  cvmlift2lem11  35529  cvmlift2lem12  35530  mrsubvrs  35738  ellcsrspsn  35857  neibastop2lem  36576  topjoin  36581  fnejoin2  36585  weiunse  36684  pibt2  37672  lindsadd  37864  poimirlem3  37874  poimirlem9  37880  poimirlem28  37899  poimirlem32  37903  prdsbnd  38044  heiborlem8  38069  rrnequiv  38086  grpokerinj  38144  0idl  38276  prnc  38318  isfldidl  38319  lshpnel2N  39361  lsatfixedN  39385  lfl0f  39445  lkrlsp3  39480  elpaddatriN  40179  elpaddat  40180  elpadd2at  40182  pmodlem1  40222  osumcllem1N  40332  osumcllem2N  40333  osumcllem9N  40340  osumcllem10N  40341  pexmidlem6N  40351  pexmidlem7N  40352  dibss  41545  dochocsn  41757  dochsncom  41758  dochnel  41769  dihprrnlem1N  41800  dihprrnlem2  41801  djhlsmat  41803  dihsmsprn  41806  dvh4dimlem  41819  dvhdimlem  41820  dochsnnz  41826  dochsatshp  41827  dochsnshp  41829  dochexmid  41844  dochsnkr  41848  dochsnkr2cl  41850  dochfl1  41852  lcfl7lem  41875  lcfl6  41876  lcfl8  41878  lcfl9a  41881  lclkrlem2a  41883  lclkrlem2c  41885  lclkrlem2d  41886  lclkrlem2e  41887  lclkrlem2j  41892  lclkrlem2o  41897  lclkrlem2p  41898  lclkrlem2s  41901  lclkrlem2v  41904  lcfrlem14  41932  lcfrlem18  41936  lcfrlem19  41937  lcfrlem20  41938  lcfrlem23  41941  lcfrlem25  41943  lcdlkreqN  41998  mapdval4N  42008  mapdsn  42017  mapdhvmap  42145  hdmaprnlem4tN  42228  hdmapinvlem1  42294  hdmapinvlem2  42295  hdmapinvlem3  42296  hdmapinvlem4  42297  hdmapglem5  42298  hgmapvvlem3  42301  hdmapglem7a  42303  hdmapglem7b  42304  hdmapglem7  42305  hdmapoc  42307  aks6d1c5lem3  42507  deg1gprod  42510  sticksstones9  42524  sticksstones11  42526  rhmqusspan  42555  evlsbagval  42927  selvvvval  42943  0prjspnrel  42985  elrfi  43051  cmpfiiin  43054  mzpcompact2lem  43108  dfac11  43419  pwssplit4  43446  rngunsnply  43526  flcidc  43527  proot1mul  43551  iocinico  43569  cantnfresb  43681  iunrelexp0  44058  frege81d  44103  k0004lem3  44505  mnuunid  44633  binomcxplemnn0  44705  islptre  45979  limciccioolb  45981  limcicciooub  45995  limcresiooub  46000  limcresioolb  46001  ioccncflimc  46243  icccncfext  46245  icocncflimc  46247  cncfiooicc  46252  dvnprodlem2  46305  dirkercncflem2  46462  dirkercncflem3  46463  fourierdlem48  46512  fourierdlem49  46513  fourierdlem79  46543  fourierdlem101  46565  sge0sup  46749  hoidmvlelem2  46954  hoiqssbl  46983  hspmbllem1  46984  hspmbllem2  46985  ovnovollem1  47014  fsumsplitsndif  47733  imaelsetpreimafv  47755  perfectALTVlem2  48082  stgrclnbgr0  48325  isubgr3stgrlem3  48328  1hegrlfgr  48492  gsumdifsndf  48541  sepfsepc  49287  discsubc  49423  iinfconstbas  49425