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:  mapm  6975  mapsnd  6976  mapss  6979  ac6sfi  7208  fseq1p1m1  10517  seqf1oglem2  10977  sswrd  11334  resqrexlemcvg  11806  resqrexlemsqa  11811  climcvg1nlem  12139  fsumcl2lem  12189  nninfctlemfo  12841  ennnfonelemh  13352  gzsumress  13770  gzsumwsubmcl  13859  gzsumsubmcl  14231  gsumsubmclfi  14252  gsumressfi  14266  psrbaglefifi  15175  cnrest2  15479  cnptoprest2  15483  cncfss  15826  limccnpcntop  15918  dvidre  15940  dvcoapbr  15950  dvef  15970  plyaddlem  15992  plymullem  15993  plycjlemc  16003  plycn  16005  dvply2g  16009  upgruhgr  16574  umgrupgr  16575  upgr1edc  16584  umgrislfupgrdom  16594  usgrislfuspgrdom  16653  isomninnlem  17302  trilpolemisumle  17311  iswomninnlem  17323  ismkvnnlem  17326