Theorem fssd 5437

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

Syntax hints:   → wi 4   ⊆ wss 3165  ⟶wf 5266

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178  df-f 5274

This theorem is referenced by:  mapss  6777  ac6sfi  6994  fseq1p1m1  10215  seqf1oglem2  10663  sswrd  11001  resqrexlemcvg  11272  resqrexlemsqa  11277  climcvg1nlem  11602  fsumcl2lem  11651  nninfctlemfo  12303  ennnfonelemh  12717  gsumress  13169  gsumwsubmcl  13270  gsumfzsubmcl  13616  cnrest2  14650  cnptoprest2  14654  cncfss  14997  limccnpcntop  15089  dvidre  15111  dvcoapbr  15121  dvef  15141  plyaddlem  15163  plymullem  15164  plycjlemc  15174  plycn  15176  dvply2g  15180  isomninnlem  15902  trilpolemisumle  15910  iswomninnlem  15921  ismkvnnlem  15924