MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fssd Structured version   Visualization version   Unicode version

Theorem fssd 5738
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
StepHypRef Expression
1 fssd.f . 2  |-  ( ph  ->  F : A --> B )
2 fssd.b . 2  |-  ( ph  ->  B  C_  C )
3 fss 5737 . 2  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
41, 2, 3syl2anc 667 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3404   -->wf 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418  df-f 5586
This theorem is referenced by:  fconst6g  5772  tposf2  6997  mapss  7514  ralxpmap  7521  ac6sfi  7815  infpwfien  8493  infmap2  8648  cofsmo  8699  fin23lem32  8774  axdc3lem4  8883  pwfseqlem4a  9086  fseq1p1m1  11868  seqf1olem2  12253  snopiswrd  12681  wrdlen2i  13021  supcvg  13914  vdwlem8  14938  isacs2  15559  funcres2b  15802  funcestrcsetclem8  16032  funcsetcestrclem8  16047  gsumress  16519  gsumwsubmcl  16622  gsumws1  16623  pj1ghm  17353  gsumval3eu  17538  gsumval3  17541  gsumsubmcl  17552  gsumzadd  17555  gsumzoppg  17577  dprdsn  17669  pwssplit1  18282  pjdm2  19274  mat1dimelbas  19496  mat1dimmul  19501  cnrest2  20302  cnprest2  20306  1stcelcls  20476  xkoptsub  20669  pt1hmeo  20821  tsmssubm  21157  cncfss  21931  ipcn  22217  equivcau  22270  lmcau  22282  i1fmulclem  22660  i1fres  22663  mbfi1fseqlem4  22676  itg2mulclem  22704  limccnp  22846  dvcmulf  22899  dvcobr  22900  dvcnvlem  22928  dvcnv  22929  dvef  22932  elply2  23150  plyeq0lem  23164  plyaddlem  23169  plymullem  23170  dgrlem  23183  coeidlem  23191  jensenlem2  23913  jensen  23914  umgra1  25053  2trllemH  25282  constr1trl  25318  constr3trllem3  25380  eupa0  25702  eupap1  25704  minvecolem3  26518  minvecolem4  26522  minvecolem3OLD  26528  minvecolem4OLD  26532  occllem  26956  chscllem2  27291  chscllem4  27293  pjhf  27361  locfinref  28668  esumsnf  28885  poimirlem29  31969  dochpolN  35058  ismrc  35543  mapfzcons  35558  pwssplit4  35947  binomcxplemnn0  36698  climreeq  37693  limccog  37700  limcrecl  37709  limsupre  37721  limsupreOLD  37722  cncficcgt0  37766  dvdivcncf  37799  dvbdfbdioolem1  37800  ioodvbdlimc1lem1  37803  ioodvbdlimc1lem2  37804  ioodvbdlimc1lem1OLD  37805  ioodvbdlimc1lem2OLD  37806  ioodvbdlimc1  37807  ioodvbdlimc2lem  37808  ioodvbdlimc2lemOLD  37809  ioodvbdlimc2  37810  dvnprodlem2  37822  stoweidlem39  37900  stoweidlem59  37920  dirkercncflem3  37967  dirkercncf  37969  fourierdlem48  38018  fourierdlem49  38019  fourierdlem50  38020  fourierdlem51  38021  fourierdlem52  38022  fourierdlem54  38024  fourierdlem59  38029  fourierdlem70  38040  fourierdlem72  38042  fourierdlem73  38043  fourierdlem74  38044  fourierdlem75  38045  fourierdlem76  38046  fourierdlem79  38049  fourierdlem84  38054  fourierdlem85  38055  fourierdlem88  38058  fourierdlem93  38063  fourierdlem94  38064  fourierdlem96  38066  fourierdlem97  38067  fourierdlem98  38068  fourierdlem99  38069  fourierdlem102  38072  fourierdlem103  38073  fourierdlem104  38074  fourierdlem111  38081  fourierdlem112  38082  fourierdlem113  38083  fourierdlem114  38084  fouriercn  38096  elaa2lem  38097  elaa2lemOLD  38098  rrxtopnfi  38155  rrndistlt  38159  fge0icoicc  38207  fge0iccre  38216  sge0isum  38269  sge0gtfsumgt  38285  ismeannd  38305  caragenunicl  38345  caratheodorylem1  38347  caratheodorylem2  38348  isomenndlem  38351  elhoi  38364  hoicvr  38370  sge0hsphoire  38411  hoidmv1le  38416  hoiqssbllem3  38446  hspmbllem2  38449  nnsum3primesprm  38885  nnsum3primesgbe  38887  nnsum4primesodd  38891  nnsum4primesoddALTV  38892  umgrupgr  39192  upgr1e  39201  upgrres1  39380  umgrres1  39381  umgr2v2e  39562  is01wlklem  39705  funcringcsetcALTV2lem8  40098  funcringcsetclem8ALTV  40121  mapsnop  40179  mapprop  40180  zlmodzxzel  40189  snlindsntorlem  40316  refdivmptf  40406  refdivmptfv  40410  elbigolo1  40421
  Copyright terms: Public domain W3C validator