Theorem fssd 5502

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 5501	. 2 |- ( ( F : A --> B /\ B C_ C ) -> F : A --> C )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> F : A --> C )

Syntax hints:   -> wi 4   C_ 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  10391  seqf1oglem2  10845  sswrd  11188  resqrexlemcvg  11659  resqrexlemsqa  11664  climcvg1nlem  11989  fsumcl2lem  12039  nninfctlemfo  12691  ennnfonelemh  13105  gsumress  13558  gsumwsubmcl  13659  gsumfzsubmcl  14005  cnrest2  15047  cnptoprest2  15051  cncfss  15394  limccnpcntop  15486  dvidre  15508  dvcoapbr  15518  dvef  15538  plyaddlem  15560  plymullem  15561  plycjlemc  15571  plycn  15573  dvply2g  15577  upgruhgr  16052  umgrupgr  16053  upgr1edc  16062  umgrislfupgrdom  16072  usgrislfuspgrdom  16131  isomninnlem  16762  trilpolemisumle  16770  iswomninnlem  16782  ismkvnnlem  16785