Theorem fssd 5550

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 5549	. 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 5376

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 5384

This theorem is used by:  mapsnd  6974  mapss  6977  ac6sfi  7206  fseq1p1m1  10518  seqf1oglem2  10978  sswrd  11335  resqrexlemcvg  11807  resqrexlemsqa  11812  climcvg1nlem  12140  fsumcl2lem  12190  nninfctlemfo  12842  ennnfonelemh  13353  gzsumress  13771  gzsumwsubmcl  13860  gzsumsubmcl  14232  gsumsubmclfi  14253  gsumressfi  14267  psrbaglefifi  15172  cnrest2  15462  cnptoprest2  15466  cncfss  15809  limccnpcntop  15901  dvidre  15923  dvcoapbr  15933  dvef  15953  plyaddlem  15975  plymullem  15976  plycjlemc  15986  plycn  15988  dvply2g  15992  upgruhgr  16557  umgrupgr  16558  upgr1edc  16567  umgrislfupgrdom  16577  usgrislfuspgrdom  16636  isomninnlem  17285  trilpolemisumle  17294  iswomninnlem  17306  ismkvnnlem  17309