Theorem fssd 5502

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

Syntax hints:   → wi 4   ⊆ wss 3201  ⟶wf 5329

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214  df-f 5337

This theorem is referenced by:  mapss  6903  ac6sfi  7130  fseq1p1m1  10374  seqf1oglem2  10828  sswrd  11171  resqrexlemcvg  11642  resqrexlemsqa  11647  climcvg1nlem  11972  fsumcl2lem  12022  nninfctlemfo  12674  ennnfonelemh  13088  gsumress  13541  gsumwsubmcl  13642  gsumfzsubmcl  13988  cnrest2  15030  cnptoprest2  15034  cncfss  15377  limccnpcntop  15469  dvidre  15491  dvcoapbr  15501  dvef  15521  plyaddlem  15543  plymullem  15544  plycjlemc  15554  plycn  15556  dvply2g  15560  upgruhgr  16035  umgrupgr  16036  upgr1edc  16045  umgrislfupgrdom  16055  usgrislfuspgrdom  16114  isomninnlem  16745  trilpolemisumle  16753  iswomninnlem  16765  ismkvnnlem  16768