Theorem fssd 5485

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

Syntax hints:   → wi 4   ⊆ wss 3197  ⟶wf 5313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-f 5321

This theorem is referenced by:  mapss  6836  ac6sfi  7056  fseq1p1m1  10286  seqf1oglem2  10737  sswrd  11075  resqrexlemcvg  11525  resqrexlemsqa  11530  climcvg1nlem  11855  fsumcl2lem  11904  nninfctlemfo  12556  ennnfonelemh  12970  gsumress  13423  gsumwsubmcl  13524  gsumfzsubmcl  13870  cnrest2  14904  cnptoprest2  14908  cncfss  15251  limccnpcntop  15343  dvidre  15365  dvcoapbr  15375  dvef  15395  plyaddlem  15417  plymullem  15418  plycjlemc  15428  plycn  15430  dvply2g  15434  upgruhgr  15905  umgrupgr  15906  upgr1edc  15915  umgrislfupgrdom  15923  usgrislfuspgrdom  15982  isomninnlem  16357  trilpolemisumle  16365  iswomninnlem  16376  ismkvnnlem  16379