MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssd Unicode version

Theorem fssd 5745
Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fssd.f
fssd.b
Assertion
Ref Expression
fssd

Proof of Theorem fssd
StepHypRef Expression
1 fssd.f . 2
2 fssd.b . 2
3 fss 5744 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  C_wss 3475  -->wf 5589
This theorem is referenced by:  fconst6g  5779  tposf2  6998  mapss  7481  ralxpmap  7488  ac6sfi  7784  infpwfien  8464  infmap2  8619  cofsmo  8670  fin23lem32  8745  axdc3lem4  8854  pwfseqlem4a  9060  fseq1p1m1  11781  seqf1olem2  12147  snopiswrd  12556  wrdlen2i  12884  supcvg  13667  vdwlem8  14506  isacs2  15050  funcres2b  15266  gsumress  15903  gsumwsubmcl  16006  gsumws1  16007  pj1ghm  16721  gsumval3eu  16907  gsumval3  16911  gsumsubmcl  16930  gsumzadd  16935  gsumzoppg  16967  dprdsn  17083  pwssplit1  17705  pjdm2  18742  mat1dimelbas  18973  mat1dimmul  18978  cnrest2  19787  cnprest2  19791  1stcelcls  19962  xkoptsub  20155  pt1hmeo  20307  tsmssubm  20644  cncfss  21403  ipcn  21686  equivcau  21739  lmcau  21751  i1fmulclem  22109  i1fres  22112  mbfi1fseqlem4  22125  itg2mulclem  22153  limccnp  22295  dvcmulf  22348  dvcobr  22349  dvcnvlem  22377  dvcnv  22378  dvef  22381  elply2  22593  plyeq0lem  22607  plyaddlem  22612  plymullem  22613  dgrlem  22626  coeidlem  22634  jensenlem2  23317  jensen  23318  umgra1  24326  2trllemH  24554  constr1trl  24590  constr3trllem3  24652  eupa0  24974  eupap1  24976  minvecolem3  25792  minvecolem4  25796  occllem  26221  chscllem2  26556  chscllem4  26558  pjhf  26626  locfinref  27844  esumsn  28072  ismrc  30633  mapfzcons  30648  pwssplit4  31035  binomcxplemnn0  31254  climreeq  31619  limccog  31626  limcrecl  31635  limsupre  31647  cncficcgt0  31691  dvdivcncf  31724  dvbdfbdioolem1  31725  ioodvbdlimc1lem1  31728  ioodvbdlimc1lem2  31729  ioodvbdlimc1  31730  ioodvbdlimc2lem  31731  ioodvbdlimc2  31732  dvnprodlem2  31744  stoweidlem39  31821  stoweidlem59  31841  dirkercncflem3  31887  dirkercncf  31889  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem51  31940  fourierdlem52  31941  fourierdlem54  31943  fourierdlem59  31948  fourierdlem70  31959  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem79  31968  fourierdlem84  31973  fourierdlem85  31974  fourierdlem88  31977  fourierdlem93  31982  fourierdlem94  31983  fourierdlem96  31985  fourierdlem97  31986  fourierdlem98  31987  fourierdlem99  31988  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  fouriercn  32015  elaa2lem  32016  funcestrcsetclem8  32653  funcsetcestrclem8  32668  funcringcsetcOLD2lem8  32851  funcringcsetclem8OLD  32874  mapsnop  32934  mapprop  32935  zlmodzxzel  32944  snlindsntorlem  33071  dochpolN  37217
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-f 5597
  Copyright terms: Public domain W3C validator