Theorem fssd 5542

Description: Expanding the codomain of a mapping, deduction form. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
fssd.f	|- ( ph -> F : A --> B )
fssd.b	|- ( ph -> B C_ C )

Assertion

Ref	Expression
fssd	|- ( ph -> F : A --> C )

Proof of Theorem fssd

Step	Hyp	Ref	Expression
1		fssd.f	. 2 |- ( ph -> F : A --> B )
2		fssd.b	. 2 |- ( ph -> B C_ C )
3		fss 5541	. 2 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )
4	1, 2, 3	syl2anc 415	1 |- ( ph -> F : A --> C )

Syntax hints:   -> wi 4   C_ wss 3220   -->wf 5368

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 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 theorem 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 5376

This theorem is referenced by:  mapsnd  6960  mapss  6963  ac6sfi  7192  fseq1p1m1  10479  seqf1oglem2  10935  sswrd  11291  resqrexlemcvg  11763  resqrexlemsqa  11768  climcvg1nlem  12093  fsumcl2lem  12143  nninfctlemfo  12795  ennnfonelemh  13273  gzsumress  13689  gzsumwsubmcl  13778  gzsumsubmcl  14119  gsumsubmclfi  14140  gsumressfi  14144  cnrest2  15260  cnptoprest2  15264  cncfss  15607  limccnpcntop  15699  dvidre  15721  dvcoapbr  15731  dvef  15751  plyaddlem  15773  plymullem  15774  plycjlemc  15784  plycn  15786  dvply2g  15790  upgruhgr  16266  umgrupgr  16267  upgr1edc  16276  umgrislfupgrdom  16286  usgrislfuspgrdom  16345  isomninnlem  16984  trilpolemisumle  16992  iswomninnlem  17004  ismkvnnlem  17007