Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fssd GIF version

Theorem fssd 5293
 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
StepHypRef Expression
1 fssd.f . 2 (𝜑𝐹:𝐴𝐵)
2 fssd.b . 2 (𝜑𝐵𝐶)
3 fss 5292 . 2 ((𝐹:𝐴𝐵𝐵𝐶) → 𝐹:𝐴𝐶)
41, 2, 3syl2anc 409 1 (𝜑𝐹:𝐴𝐶)
 Colors of variables: wff set class Syntax hints:   → wi 4   ⊆ wss 3076  ⟶wf 5127 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089  df-f 5135 This theorem is referenced by:  mapss  6593  ac6sfi  6800  fseq1p1m1  9905  resqrexlemcvg  10823  resqrexlemsqa  10828  climcvg1nlem  11150  fsumcl2lem  11199  ennnfonelemh  11953  cnrest2  12444  cnptoprest2  12448  cncfss  12778  limccnpcntop  12852  dvcoapbr  12879  dvef  12896  isomninnlem  13400  trilpolemisumle  13406  iswomninnlem  13417  ismkvnnlem  13419
 Copyright terms: Public domain W3C validator