Theorem fssd 6730

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 6729	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4	1, 2, 3	syl2anc 596	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3896  ⟶wf 6537

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

This proof depends on definitions:  df-bi 210  df-an 402  df-ss 3897  df-f 6545

This theorem is used by:  fconst6g  6774  f1ounsn  7282  fsnex  7293  tposf2  8272  mapsnd  8919  mapss  8922  ralxpmap  8929  ac6sfi  9280  infpwfien  10146  infmap2  10300  cofsmo  10352  fin23lem32  10427  axdc3lem4  10536  pwfseqlem4a  10751  fseq1p1m1  13737  seqf1olem2  14190  wrdlen2i  15100  supcvg  16032  vdwlem8  17173  isacs2  17834  funcres2b  18079  funcestrcsetclem8  18328  funcsetcestrclem8  18343  gsumress  18878  gsumwsubmcl  19040  gsumws1  19041  pj1ghm  19924  gsumval3eu  20125  gsumval3  20128  gsumsubmcl  20140  gsumzadd  20143  gsumzoppg  20165  dprdsn  20259  pwssplit1  21341  pjdm2  22024  evlsvvval  22409  psdmul  22494  mat1dimelbas  22793  cnrest2  23611  cnprest2  23615  1stcelcls  23787  xkoptsub  23980  tsmssubm  24469  cncfss  25227  ipcn  25574  equivcau  25628  lmcau  25641  rrx0el  25726  i1fmulclem  26030  i1fres  26033  mbfi1fseqlem4  26046  itg2mulclem  26074  limccnp  26218  dvcmulf  26272  dvcobr  26273  dvcnvlem  26303  dvcnv  26304  dvef  26307  elply2  26521  plyeq0lem  26536  plyaddlem  26541  plymullem  26542  dgrlem  26555  coeidlem  26563  jensenlem2  27322  jensen  27323  om2noseqlt  28692  om2noseqlt2  28693  om2noseqf1o  28694  umgrupgr  29688  upgr1e  29698  umgrislfupgr  29708  usgrislfuspgr  29775  upgrres1  29901  umgrres1  29902  umgr2v2e  30113  0clwlkv  30729  minvecolem3  31485  minvecolem4  31489  occllem  31912  chscllem2  32247  chscllem4  32249  pjhf  32317  elrgspnsubrunlem1  33856  gsumind  33954  islinds5  33971  ellspds  33972  linds2eq  33984  1arithidomlem2  34116  1arithidom  34117  dfufd2lem  34129  selvply1rhmlemb  34199  mplmulmvr  34219  psrmonprod  34232  mplgsum  34233  esplyfval0  34244  esplylem  34246  esplympl  34247  esplyfv1  34249  esplyfval3  34252  esplyfval1  34253  esplyfvaln  34254  esplyind  34255  fedgmullem1  34309  fedgmullem2  34310  locfinref  34521  esumsnf  34744  hashreprin  35297  poimirlem29  38674  dochpolN  42654  aks6d1c7lem1  43337  evlsbagval  43721  evlsmhpvvval  43730  mhphf  43732  ismrc  43819  mapfzcons  43834  pwssplit4  44198  ntrf2  45231  binomcxplemnn0  45440  fcomptss  46324  fcoss  46330  frexr  46503  climreeq  46732  limccog  46739  limcrecl  46748  limsupre  46758  liminflimsupclim  46924  cncficcgt0  47005  dvdivcncf  47044  dvbdfbdioolem1  47045  ioodvbdlimc1lem1  47048  ioodvbdlimc1lem2  47049  ioodvbdlimc1  47050  ioodvbdlimc2lem  47051  ioodvbdlimc2  47052  dvnprodlem2  47064  voliooicof  47113  volicofmpt  47114  stoweidlem39  47156  stoweidlem59  47176  dirkercncflem3  47222  dirkercncf  47224  fourierdlem48  47271  fourierdlem49  47272  fourierdlem50  47273  fourierdlem51  47274  fourierdlem52  47275  fourierdlem54  47277  fourierdlem59  47282  fourierdlem70  47293  fourierdlem72  47295  fourierdlem73  47296  fourierdlem74  47297  fourierdlem75  47298  fourierdlem76  47299  fourierdlem79  47302  fourierdlem84  47307  fourierdlem85  47308  fourierdlem88  47311  fourierdlem93  47316  fourierdlem94  47317  fourierdlem96  47319  fourierdlem97  47320  fourierdlem98  47321  fourierdlem99  47322  fourierdlem102  47325  fourierdlem103  47326  fourierdlem104  47327  fourierdlem111  47334  fourierdlem112  47335  fourierdlem113  47336  fourierdlem114  47337  fouriercn  47349  elaa2lem  47350  rrxtopnfi  47404  rrndistlt  47407  ioorrnopnlem  47421  issalnnd  47462  fge0icoicc  47482  fge0iccre  47491  sge0isum  47544  sge0gtfsumgt  47560  sge0seq  47563  ismeannd  47584  meaiuninclem  47597  caragenunicl  47641  caratheodorylem1  47643  caratheodorylem2  47644  isomenndlem  47647  elhoi  47659  sge0hsphoire  47706  hoidmv1le  47711  hoiqssbllem3  47741  hspmbllem2  47744  ovolval2lem  47760  ovolval3  47764  ovolval4lem2  47767  ovolval5lem2  47770  ovnovollem1  47773  ovnovollem2  47774  iunhoiioolem  47792  iccvonmbllem  47795  vonioolem2  47798  vonioo  47799  smfco  47919  nnsum3primesgbe  48997  nnsum4primesodd  49001  nnsum4primesoddALTV  49002  grimuhgr  49092  uhgrimisgrgric  49136  isubgr3stgrlem6  49176  1hegrlfgr  49337  funcringcsetcALTV2lem8  49501  funcringcsetclem8ALTV  49524  mapsnop  49563  fprmappr  49564  zlmodzxzel  49574  snlindsntorlem  49689  refdivmptf  49761  refdivmptfv  49765  elbigolo1  49776  2arymaptfo  49873  line2  49971  amgmwlem  51169