Theorem fssd 6724

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902  ⟶wf 6533

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 3919  df-f 6541

This theorem is used by:  fconst6g  6768  f1ounsn  7277  fsnex  7288  tposf2  8252  mapsnd  8897  mapss  8900  ralxpmap  8907  ac6sfi  9258  infpwfien  10069  infmap2  10223  cofsmo  10275  fin23lem32  10350  axdc3lem4  10459  pwfseqlem4a  10674  fseq1p1m1  13657  seqf1olem2  14110  wrdlen2i  15017  supcvg  15949  vdwlem8  17086  isacs2  17747  funcres2b  17992  funcestrcsetclem8  18241  funcsetcestrclem8  18256  gsumress  18790  gsumwsubmcl  18952  gsumws1  18953  pj1ghm  19836  gsumval3eu  20037  gsumval3  20040  gsumsubmcl  20052  gsumzadd  20055  gsumzoppg  20077  dprdsn  20171  pwssplit1  21249  pjdm2  21930  evlsvvval  22315  psdmul  22400  mat1dimelbas  22699  cnrest2  23517  cnprest2  23521  1stcelcls  23693  xkoptsub  23886  tsmssubm  24375  cncfss  25133  ipcn  25480  equivcau  25534  lmcau  25547  rrx0el  25632  i1fmulclem  25936  i1fres  25939  mbfi1fseqlem4  25952  itg2mulclem  25980  limccnp  26125  dvcmulf  26179  dvcobr  26180  dvcnvlem  26210  dvcnv  26211  dvef  26214  elply2  26428  plyeq0lem  26443  plyaddlem  26448  plymullem  26449  dgrlem  26462  coeidlem  26470  jensenlem2  27232  jensen  27233  om2noseqlt  28572  om2noseqlt2  28573  om2noseqf1o  28574  umgrupgr  29568  upgr1e  29578  umgrislfupgr  29588  usgrislfuspgr  29655  upgrres1  29781  umgrres1  29782  umgr2v2e  29993  0clwlkv  30609  minvecolem3  31365  minvecolem4  31369  occllem  31792  chscllem2  32127  chscllem4  32129  pjhf  32197  elrgspnsubrunlem1  33695  gsumind  33793  islinds5  33810  ellspds  33811  linds2eq  33822  1arithidomlem2  33954  1arithidom  33955  dfufd2lem  33967  selvply1rhmlemb  34037  mplmulmvr  34057  psrmonprod  34070  mplgsum  34071  esplyfval0  34082  esplylem  34084  esplympl  34085  esplyfv1  34087  esplyfval3  34090  esplyfval1  34091  esplyfvaln  34092  esplyind  34093  fedgmullem1  34147  fedgmullem2  34148  locfinref  34359  esumsnf  34582  hashreprin  35136  poimirlem29  38406  dochpolN  42371  aks6d1c7lem1  43054  evlsbagval  43440  evlsmhpvvval  43449  mhphf  43451  ismrc  43554  mapfzcons  43569  pwssplit4  43938  ntrf2  44972  binomcxplemnn0  45181  fcomptss  46042  fcoss  46048  frexr  46222  climreeq  46451  limccog  46458  limcrecl  46467  limsupre  46477  liminflimsupclim  46643  cncficcgt0  46724  dvdivcncf  46763  dvbdfbdioolem1  46764  ioodvbdlimc1lem1  46767  ioodvbdlimc1lem2  46768  ioodvbdlimc1  46769  ioodvbdlimc2lem  46770  ioodvbdlimc2  46771  dvnprodlem2  46783  voliooicof  46832  volicofmpt  46833  stoweidlem39  46875  stoweidlem59  46895  dirkercncflem3  46941  dirkercncf  46943  fourierdlem48  46990  fourierdlem49  46991  fourierdlem50  46992  fourierdlem51  46993  fourierdlem52  46994  fourierdlem54  46996  fourierdlem59  47001  fourierdlem70  47012  fourierdlem72  47014  fourierdlem73  47015  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem79  47021  fourierdlem84  47026  fourierdlem85  47027  fourierdlem88  47030  fourierdlem93  47035  fourierdlem94  47036  fourierdlem96  47038  fourierdlem97  47039  fourierdlem98  47040  fourierdlem99  47041  fourierdlem102  47044  fourierdlem103  47045  fourierdlem104  47046  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  fourierdlem114  47056  fouriercn  47068  elaa2lem  47069  rrxtopnfi  47123  rrndistlt  47126  ioorrnopnlem  47140  issalnnd  47181  fge0icoicc  47201  fge0iccre  47210  sge0isum  47263  sge0gtfsumgt  47279  sge0seq  47282  ismeannd  47303  meaiuninclem  47316  caragenunicl  47360  caratheodorylem1  47362  caratheodorylem2  47363  isomenndlem  47366  elhoi  47378  sge0hsphoire  47425  hoidmv1le  47430  hoiqssbllem3  47460  hspmbllem2  47463  ovolval2lem  47479  ovolval3  47483  ovolval4lem2  47486  ovolval5lem2  47489  ovnovollem1  47492  ovnovollem2  47493  iunhoiioolem  47511  iccvonmbllem  47514  vonioolem2  47517  vonioo  47518  smfco  47638  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  grimuhgr  48811  uhgrimisgrgric  48855  isubgr3stgrlem6  48895  1hegrlfgr  49056  funcringcsetcALTV2lem8  49220  funcringcsetclem8ALTV  49243  mapsnop  49282  fprmappr  49283  zlmodzxzel  49293  snlindsntorlem  49408  refdivmptf  49480  refdivmptfv  49484  elbigolo1  49495  2arymaptfo  49592  prelrrx2  49651  line2  49690  line2x  49692  line2y  49693  amgmwlem  50828