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

Theorem fssd 5722
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 5721 . 2  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
41, 2, 3syl2anc 659 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3461   -->wf 5566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475  df-f 5574
This theorem is referenced by:  fconst6g  5756  tposf2  6971  mapss  7454  ralxpmap  7461  ac6sfi  7756  infpwfien  8434  infmap2  8589  cofsmo  8640  fin23lem32  8715  axdc3lem4  8824  pwfseqlem4a  9028  fseq1p1m1  11756  seqf1olem2  12129  snopiswrd  12543  wrdlen2i  12875  supcvg  13749  vdwlem8  14590  isacs2  15142  funcres2b  15385  funcestrcsetclem8  15615  funcsetcestrclem8  15630  gsumress  16102  gsumwsubmcl  16205  gsumws1  16206  pj1ghm  16920  gsumval3eu  17106  gsumval3  17110  gsumsubmcl  17129  gsumzadd  17134  gsumzoppg  17165  dprdsn  17278  pwssplit1  17900  pjdm2  18915  mat1dimelbas  19140  mat1dimmul  19145  cnrest2  19954  cnprest2  19958  1stcelcls  20128  xkoptsub  20321  pt1hmeo  20473  tsmssubm  20810  cncfss  21569  ipcn  21852  equivcau  21905  lmcau  21917  i1fmulclem  22275  i1fres  22278  mbfi1fseqlem4  22291  itg2mulclem  22319  limccnp  22461  dvcmulf  22514  dvcobr  22515  dvcnvlem  22543  dvcnv  22544  dvef  22547  elply2  22759  plyeq0lem  22773  plyaddlem  22778  plymullem  22779  dgrlem  22792  coeidlem  22800  jensenlem2  23515  jensen  23516  umgra1  24528  2trllemH  24756  constr1trl  24792  constr3trllem3  24854  eupa0  25176  eupap1  25178  minvecolem3  25990  minvecolem4  25994  occllem  26419  chscllem2  26754  chscllem4  26756  pjhf  26824  locfinref  28079  esumsnf  28293  ismrc  30873  mapfzcons  30888  pwssplit4  31274  binomcxplemnn0  31495  climreeq  31858  limccog  31865  limcrecl  31874  limsupre  31886  cncficcgt0  31930  dvdivcncf  31963  dvbdfbdioolem1  31964  ioodvbdlimc1lem1  31967  ioodvbdlimc1lem2  31968  ioodvbdlimc1  31969  ioodvbdlimc2lem  31970  ioodvbdlimc2  31971  dvnprodlem2  31983  stoweidlem39  32060  stoweidlem59  32080  dirkercncflem3  32126  dirkercncf  32128  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem52  32180  fourierdlem54  32182  fourierdlem59  32187  fourierdlem70  32198  fourierdlem72  32200  fourierdlem73  32201  fourierdlem74  32202  fourierdlem75  32203  fourierdlem76  32204  fourierdlem79  32207  fourierdlem84  32212  fourierdlem85  32213  fourierdlem88  32216  fourierdlem93  32221  fourierdlem94  32222  fourierdlem96  32224  fourierdlem97  32225  fourierdlem98  32226  fourierdlem99  32227  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem111  32239  fourierdlem112  32240  fourierdlem113  32241  fourierdlem114  32242  fouriercn  32254  elaa2lem  32255  funcringcsetcALTV2lem8  33105  funcringcsetclem8ALTV  33128  mapsnop  33188  mapprop  33189  zlmodzxzel  33198  snlindsntorlem  33325  refdivmptf  33417  refdivmptfv  33421  elbigolo1  33432  dochpolN  37614
  Copyright terms: Public domain W3C validator