Theorem fssd 5495

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

Hypotheses

Ref	Expression
fssd.f	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
fssd.b	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
fssd	⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Proof of Theorem fssd

Step	Hyp	Ref	Expression
1		fssd.f	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		fssd.b	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
3		fss 5494	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐵 ⊆ 𝐶) → 𝐹:𝐴⟶𝐶)
4	1, 2, 3	syl2anc 411	1 ⊢ (𝜑 → 𝐹:𝐴⟶𝐶)

Syntax hints:   → wi 4   ⊆ wss 3200  ⟶wf 5322

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213  df-f 5330

This theorem is referenced by:  mapss  6859  ac6sfi  7086  fseq1p1m1  10328  seqf1oglem2  10781  sswrd  11121  resqrexlemcvg  11579  resqrexlemsqa  11584  climcvg1nlem  11909  fsumcl2lem  11958  nninfctlemfo  12610  ennnfonelemh  13024  gsumress  13477  gsumwsubmcl  13578  gsumfzsubmcl  13924  cnrest2  14959  cnptoprest2  14963  cncfss  15306  limccnpcntop  15398  dvidre  15420  dvcoapbr  15430  dvef  15450  plyaddlem  15472  plymullem  15473  plycjlemc  15483  plycn  15485  dvply2g  15489  upgruhgr  15961  umgrupgr  15962  upgr1edc  15971  umgrislfupgrdom  15981  usgrislfuspgrdom  16040  isomninnlem  16634  trilpolemisumle  16642  iswomninnlem  16653  ismkvnnlem  16656