Theorem fssd 6757

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

Step	Hyp	Ref	Expression
1		fssd.f	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fssd.b	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		fss 6756	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3901  df-f 6570

This theorem is used by:  fconst6g  6801  f1ounsn  7311  fsnex  7322  tposf2  8305  mapsnd  8952  mapss  8955  ralxpmap  8962  ac6sfi  9313  infpwfien  10180  infmap2  10334  cofsmo  10386  fin23lem32  10461  axdc3lem4  10570  pwfseqlem4a  10785  fseq1p1m1  13772  seqf1olem2  14225  wrdlen2i  15136  supcvg  16069  vdwlem8  17210  isacs2  17877  funcres2b  18122  funcestrcsetclem8  18371  funcsetcestrclem8  18386  gsumress  18921  gsumwsubmcl  19083  gsumws1  19084  pj1ghm  19968  gsumval3eu  20169  gsumval3  20172  gsumsubmcl  20184  gsumzadd  20187  gsumzoppg  20209  dprdsn  20303  pwssplit1  21385  pjdm2  22072  evlsvvval  22457  psdmul  22542  mat1dimelbas  22841  cnrest2  23659  cnprest2  23663  1stcelcls  23835  xkoptsub  24028  tsmssubm  24517  cncfss  25275  ipcn  25622  equivcau  25676  lmcau  25689  rrx0el  25774  i1fmulclem  26078  i1fres  26081  mbfi1fseqlem4  26094  itg2mulclem  26122  limccnp  26266  dvcmulf  26320  dvcobr  26321  dvcnvlem  26351  dvcnv  26352  dvef  26355  elply2  26569  plyeq0lem  26584  plyaddlem  26589  plymullem  26590  dgrlem  26603  coeidlem  26611  jensenlem2  27372  jensen  27373  om2noseqlt  28742  om2noseqlt2  28743  om2noseqf1o  28744  umgrupgr  29738  upgr1e  29748  umgrislfupgr  29758  usgrislfuspgr  29825  upgrres1  29951  umgrres1  29952  umgr2v2e  30163  0clwlkv  30779  minvecolem3  31535  minvecolem4  31539  occllem  31962  chscllem2  32297  chscllem4  32299  pjhf  32367  elrgspnsubrunlem1  33907  gsumind  34010  islinds5  34027  ellspds  34028  linds2eq  34040  1arithidomlem2  34172  1arithidom  34173  dfufd2lem  34185  selvply1rhmlemb  34262  mplmulmvr  34282  psrmonprod  34295  mplgsum  34296  esplyfval0  34307  esplylem  34309  esplympl  34310  esplyfv1  34312  esplyfval3  34315  esplyfval1  34316  esplyfvaln  34317  esplyind  34318  fedgmullem1  34372  fedgmullem2  34373  locfinref  34584  esumsnf  34807  hashreprin  35360  poimirlem29  38835  dochpolN  42813  aks6d1c7lem1  43496  evlsbagval  43880  evlsmhpvvval  43889  mhphf  43891  ismrc  43978  mapfzcons  43993  pwssplit4  44357  ntrf2  45385  binomcxplemnn0  45594  fcomptss  46490  fcoss  46496  frexr  46669  climreeq  46898  limccog  46905  limcrecl  46914  limsupre  46924  liminflimsupclim  47090  cncficcgt0  47171  dvdivcncf  47210  dvbdfbdioolem1  47211  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc1  47216  ioodvbdlimc2lem  47217  ioodvbdlimc2  47218  dvnprodlem2  47230  voliooicof  47279  volicofmpt  47280  stoweidlem39  47322  stoweidlem59  47342  dirkercncflem3  47388  dirkercncf  47390  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem51  47440  fourierdlem52  47441  fourierdlem54  47443  fourierdlem59  47448  fourierdlem70  47459  fourierdlem72  47461  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem79  47468  fourierdlem84  47473  fourierdlem85  47474  fourierdlem88  47477  fourierdlem93  47482  fourierdlem94  47483  fourierdlem96  47485  fourierdlem97  47486  fourierdlem98  47487  fourierdlem99  47488  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  fourierdlem114  47503  fouriercn  47515  elaa2lem  47516  rrxtopnfi  47570  rrndistlt  47573  ioorrnopnlem  47587  issalnnd  47628  fge0icoicc  47648  fge0iccre  47657  sge0isum  47710  sge0gtfsumgt  47726  sge0seq  47729  ismeannd  47750  meaiuninclem  47763  caragenunicl  47807  caratheodorylem1  47809  caratheodorylem2  47810  isomenndlem  47813  elhoi  47825  sge0hsphoire  47872  hoidmv1le  47877  hoiqssbllem3  47907  hspmbllem2  47910  ovolval2lem  47926  ovolval3  47930  ovolval4lem2  47933  ovolval5lem2  47936  ovnovollem1  47939  ovnovollem2  47940  iunhoiioolem  47958  iccvonmbllem  47961  vonioolem2  47964  vonioo  47965  smfco  48085  nnsum3primesgbe  49163  nnsum4primesodd  49167  nnsum4primesoddALTV  49168  grimuhgr  49258  uhgrimisgrgric  49302  isubgr3stgrlem6  49342  1hegrlfgr  49503  funcringcsetcALTV2lem8  49667  funcringcsetclem8ALTV  49690  mapsnop  49787  fprmappr  49788  zlmodzxzel  49798  snlindsntorlem  49913  refdivmptf  49985  refdivmptfv  49989  elbigolo1  50000  2arymaptfo  50097  line2  50195  amgmwlem  51415