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  10501  seqf1oglem2  10957  sswrd  11313  resqrexlemcvg  11785  resqrexlemsqa  11790  climcvg1nlem  12115  fsumcl2lem  12165  nninfctlemfo  12817  ennnfonelemh  13295  gzsumress  13712  gzsumwsubmcl  13801  gzsumsubmcl  14142  gsumsubmclfi  14163  gsumressfi  14167  cnrest2  15337  cnptoprest2  15341  cncfss  15684  limccnpcntop  15776  dvidre  15798  dvcoapbr  15808  dvef  15828  plyaddlem  15850  plymullem  15851  plycjlemc  15861  plycn  15863  dvply2g  15867  upgruhgr  16352  umgrupgr  16353  upgr1edc  16362  umgrislfupgrdom  16372  usgrislfuspgrdom  16431  isomninnlem  17079  trilpolemisumle  17087  iswomninnlem  17099  ismkvnnlem  17102