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

Theorem fssd 5753
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 5752 . 2  |-  ( ( F : A --> B  /\  B  C_  C )  ->  F : A --> C )
41, 2, 3syl2anc 666 1  |-  ( ph  ->  F : A --> C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3437   -->wf 5595
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3444  df-ss 3451  df-f 5603
This theorem is referenced by:  fconst6g  5787  tposf2  7003  mapss  7520  ralxpmap  7527  ac6sfi  7819  infpwfien  8495  infmap2  8650  cofsmo  8701  fin23lem32  8776  axdc3lem4  8885  pwfseqlem4a  9088  fseq1p1m1  11870  seqf1olem2  12254  snopiswrd  12679  wrdlen2i  13015  supcvg  13907  vdwlem8  14931  isacs2  15552  funcres2b  15795  funcestrcsetclem8  16025  funcsetcestrclem8  16040  gsumress  16512  gsumwsubmcl  16615  gsumws1  16616  pj1ghm  17346  gsumval3eu  17531  gsumval3  17534  gsumsubmcl  17545  gsumzadd  17548  gsumzoppg  17570  dprdsn  17662  pwssplit1  18275  pjdm2  19266  mat1dimelbas  19488  mat1dimmul  19493  cnrest2  20294  cnprest2  20298  1stcelcls  20468  xkoptsub  20661  pt1hmeo  20813  tsmssubm  21149  cncfss  21923  ipcn  22209  equivcau  22262  lmcau  22274  i1fmulclem  22652  i1fres  22655  mbfi1fseqlem4  22668  itg2mulclem  22696  limccnp  22838  dvcmulf  22891  dvcobr  22892  dvcnvlem  22920  dvcnv  22921  dvef  22924  elply2  23142  plyeq0lem  23156  plyaddlem  23161  plymullem  23162  dgrlem  23175  coeidlem  23183  jensenlem2  23905  jensen  23906  umgra1  25045  2trllemH  25274  constr1trl  25310  constr3trllem3  25372  eupa0  25694  eupap1  25696  minvecolem3  26510  minvecolem4  26514  minvecolem3OLD  26520  minvecolem4OLD  26524  occllem  26948  chscllem2  27283  chscllem4  27285  pjhf  27353  locfinref  28670  esumsnf  28887  poimirlem29  31927  dochpolN  35021  ismrc  35506  mapfzcons  35521  pwssplit4  35911  binomcxplemnn0  36600  climreeq  37557  limccog  37564  limcrecl  37573  limsupre  37585  limsupreOLD  37586  cncficcgt0  37630  dvdivcncf  37663  dvbdfbdioolem1  37664  ioodvbdlimc1lem1  37667  ioodvbdlimc1lem2  37668  ioodvbdlimc1lem1OLD  37669  ioodvbdlimc1lem2OLD  37670  ioodvbdlimc1  37671  ioodvbdlimc2lem  37672  ioodvbdlimc2lemOLD  37673  ioodvbdlimc2  37674  dvnprodlem2  37686  stoweidlem39  37764  stoweidlem59  37784  dirkercncflem3  37831  dirkercncf  37833  fourierdlem48  37882  fourierdlem49  37883  fourierdlem50  37884  fourierdlem51  37885  fourierdlem52  37886  fourierdlem54  37888  fourierdlem59  37893  fourierdlem70  37904  fourierdlem72  37906  fourierdlem73  37907  fourierdlem74  37908  fourierdlem75  37909  fourierdlem76  37910  fourierdlem79  37913  fourierdlem84  37918  fourierdlem85  37919  fourierdlem88  37922  fourierdlem93  37927  fourierdlem94  37928  fourierdlem96  37930  fourierdlem97  37931  fourierdlem98  37932  fourierdlem99  37933  fourierdlem102  37936  fourierdlem103  37937  fourierdlem104  37938  fourierdlem111  37945  fourierdlem112  37946  fourierdlem113  37947  fourierdlem114  37948  fouriercn  37960  elaa2lem  37961  elaa2lemOLD  37962  fge0icoicc  38039  fge0iccre  38048  sge0isum  38101  ismeannd  38128  caragenunicl  38168  caratheodorylem1  38170  caratheodorylem2  38171  isomenndlem  38174  elhoi  38183  hoicvr  38189  nnsum3primesprm  38641  nnsum3primesgbe  38643  nnsum4primesodd  38647  nnsum4primesoddALTV  38648  umgr1  38894  funcringcsetcALTV2lem8  39387  funcringcsetclem8ALTV  39410  mapsnop  39470  mapprop  39471  zlmodzxzel  39480  snlindsntorlem  39607  refdivmptf  39697  refdivmptfv  39701  elbigolo1  39712
  Copyright terms: Public domain W3C validator