Theorem fssd 5547

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

This proof depends on syntax axioms:   -> wi 4   C_ 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  10511  seqf1oglem2  10970  sswrd  11327  resqrexlemcvg  11799  resqrexlemsqa  11804  climcvg1nlem  12131  fsumcl2lem  12181  nninfctlemfo  12833  ennnfonelemh  13344  gzsumress  13761  gzsumwsubmcl  13850  gzsumsubmcl  14191  gsumsubmclfi  14212  gsumressfi  14216  cnrest2  15386  cnptoprest2  15390  cncfss  15733  limccnpcntop  15825  dvidre  15847  dvcoapbr  15857  dvef  15877  plyaddlem  15899  plymullem  15900  plycjlemc  15910  plycn  15912  dvply2g  15916  upgruhgr  16450  umgrupgr  16451  upgr1edc  16460  umgrislfupgrdom  16470  usgrislfuspgrdom  16529  isomninnlem  17177  trilpolemisumle  17185  iswomninnlem  17197  ismkvnnlem  17200