Theorem fssd 5547

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3220  ⟶wf 5373

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233  df-f 5381

This theorem is used by:  mapsnd  6970  mapss  6973  ac6sfi  7202  fseq1p1m1  10512  seqf1oglem2  10972  sswrd  11329  resqrexlemcvg  11801  resqrexlemsqa  11806  climcvg1nlem  12134  fsumcl2lem  12184  nninfctlemfo  12836  ennnfonelemh  13347  gzsumress  13765  gzsumwsubmcl  13854  gzsumsubmcl  14226  gsumsubmclfi  14247  gsumressfi  14251  psrbaglefifi  15147  cnrest2  15428  cnptoprest2  15432  cncfss  15775  limccnpcntop  15867  dvidre  15889  dvcoapbr  15899  dvef  15919  plyaddlem  15941  plymullem  15942  plycjlemc  15952  plycn  15954  dvply2g  15958  upgruhgr  16518  umgrupgr  16519  upgr1edc  16528  umgrislfupgrdom  16538  usgrislfuspgrdom  16597  isomninnlem  17245  trilpolemisumle  17254  iswomninnlem  17266  ismkvnnlem  17269