Theorem fssd 6764

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

Syntax hints:   → wi 4   ⊆ wss 3976  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807

This theorem depends on definitions:  df-bi 207  df-an 396  df-ss 3993  df-f 6577

This theorem is referenced by:  fco3OLD  6781  fconst6g  6810  fsnex  7319  tposf2  8291  mapsnd  8944  mapss  8947  ralxpmap  8954  ac6sfi  9348  infpwfien  10131  infmap2  10286  cofsmo  10338  fin23lem32  10413  axdc3lem4  10522  pwfseqlem4a  10730  fseq1p1m1  13658  seqf1olem2  14093  wrdlen2i  14991  supcvg  15904  vdwlem8  17035  isacs2  17711  funcres2b  17961  funcestrcsetclem8  18216  funcsetcestrclem8  18231  gsumress  18720  gsumwsubmcl  18872  gsumws1  18873  pj1ghm  19745  gsumval3eu  19946  gsumval3  19949  gsumsubmcl  19961  gsumzadd  19964  gsumzoppg  19986  dprdsn  20080  pwssplit1  21081  pjdm2  21754  psdmul  22193  mat1dimelbas  22498  cnrest2  23315  cnprest2  23319  1stcelcls  23490  xkoptsub  23683  tsmssubm  24172  cncfss  24944  ipcn  25299  equivcau  25353  lmcau  25366  rrx0el  25451  i1fmulclem  25757  i1fres  25760  mbfi1fseqlem4  25773  itg2mulclem  25801  limccnp  25946  dvcmulf  26002  dvcobr  26003  dvcobrOLD  26004  dvcnvlem  26034  dvcnv  26035  dvef  26038  elply2  26255  plyeq0lem  26269  plyaddlem  26274  plymullem  26275  dgrlem  26288  coeidlem  26296  jensenlem2  27049  jensen  27050  om2noseqlt  28323  om2noseqlt2  28324  om2noseqf1o  28325  umgrupgr  29138  upgr1e  29148  umgrislfupgr  29158  usgrislfuspgr  29222  upgrres1  29348  umgrres1  29349  umgr2v2e  29561  0clwlkv  30163  minvecolem3  30908  minvecolem4  30912  occllem  31335  chscllem2  31670  chscllem4  31672  pjhf  31740  islinds5  33360  ellspds  33361  linds2eq  33374  1arithidomlem2  33529  1arithidom  33530  dfufd2lem  33542  fedgmullem1  33642  fedgmullem2  33643  locfinref  33787  esumsnf  34028  hashreprin  34597  poimirlem29  37609  dochpolN  41447  aks6d1c7lem1  42137  evlsvvval  42518  evlsbagval  42521  evlsmhpvvval  42550  mhphf  42552  ismrc  42657  mapfzcons  42672  pwssplit4  43046  ntrf2  44086  binomcxplemnn0  44318  fcomptss  45110  fcoss  45117  frexr  45300  climreeq  45534  limccog  45541  limcrecl  45550  limsupre  45562  liminflimsupclim  45728  cncficcgt0  45809  dvdivcncf  45848  dvbdfbdioolem1  45849  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc1  45854  ioodvbdlimc2lem  45855  ioodvbdlimc2  45856  dvnprodlem2  45868  voliooicof  45917  volicofmpt  45918  stoweidlem39  45960  stoweidlem59  45980  dirkercncflem3  46026  dirkercncf  46028  fourierdlem48  46075  fourierdlem49  46076  fourierdlem50  46077  fourierdlem51  46078  fourierdlem52  46079  fourierdlem54  46081  fourierdlem59  46086  fourierdlem70  46097  fourierdlem72  46099  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem79  46106  fourierdlem84  46111  fourierdlem85  46112  fourierdlem88  46115  fourierdlem93  46120  fourierdlem94  46121  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fourierdlem114  46141  fouriercn  46153  elaa2lem  46154  rrxtopnfi  46208  rrndistlt  46211  ioorrnopnlem  46225  issalnnd  46266  fge0icoicc  46286  fge0iccre  46295  sge0isum  46348  sge0gtfsumgt  46364  sge0seq  46367  ismeannd  46388  meaiuninclem  46401  caragenunicl  46445  caratheodorylem1  46447  caratheodorylem2  46448  isomenndlem  46451  elhoi  46463  hoicvr  46469  sge0hsphoire  46510  hoidmv1le  46515  hoiqssbllem3  46545  hspmbllem2  46548  ovolval2lem  46564  ovolval3  46568  ovolval4lem2  46571  ovolval5lem2  46574  ovnovollem1  46577  ovnovollem2  46578  iunhoiioolem  46596  iccvonmbllem  46599  vonioolem2  46602  vonioo  46603  smfco  46723  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  grimuhgr  47762  uhgrimisgrgric  47783  1hegrlfgr  47855  funcringcsetcALTV2lem8  48020  funcringcsetclem8ALTV  48043  mapsnop  48069  fprmappr  48070  zlmodzxzel  48080  snlindsntorlem  48199  refdivmptf  48276  refdivmptfv  48280  elbigolo1  48291  2arymaptfo  48388  prelrrx2  48447  line2  48486  line2x  48488  line2y  48489  amgmwlem  48896