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

Theorem ffvelrnda 5748
Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)
Hypothesis
Ref Expression
ffvelrnd.1  |-  ( ph  ->  F : A --> B )
Assertion
Ref Expression
ffvelrnda  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )

Proof of Theorem ffvelrnda
StepHypRef Expression
1 ffvelrnd.1 . 2  |-  ( ph  ->  F : A --> B )
2 ffvelrn 5746 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 457 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1710   -->wf 5333   ` cfv 5337
This theorem is referenced by:  ffvelrnd  5749  iunfictbso  7831  cofucl  13861  cofulid  13863  funcres2b  13870  funcpropd  13873  ffthiso  13902  fuccocl  13937  fucidcl  13938  fuclid  13939  fucrid  13940  fucass  13941  fucsect  13945  fucinv  13946  invfuc  13947  fuciso  13948  natpropd  13949  fucpropd  13950  setcepi  14019  catcisolem  14037  prfcl  14076  prf1st  14077  prf2nd  14078  1st2ndprf  14079  evlfcl  14095  curfuncf  14111  hofcl  14132  yonedalem4c  14150  yonedainv  14154  yonffthlem  14155  negfcncf  18526  ellimc2  19331  limcres  19340  cmvth  19442  lhop1lem  19464  lhop1  19465  lhop2  19466  lhop  19467  ftc1lem6  19492  dvply2g  19769  aannenlem1  19812  aannenlem2  19813  taylthlem1  19856  taylthlem2  19857  ulmdvlem1  19883  mtestbdd  19888  iunrdx  23213  disjrdx  23229  xppreima2  23263  ofoprabco  23283  isoun  23293  rhmdvdsr  23422  neiptopnei  23445  tpr2rico  23466  lmxrge0  23493  lmdvg  23494  indsum  23686  indpreima  23688  esumf1o  23711  esumpcvgval  23734  ofcf  23752  measvuni  23832  meascnbl  23837  volmeas  23851  mbfmco2  23879  rrvsum  23961  dstfrvunirn  23981  lgamgulmlem6  24067  lgamgulm2  24069  gamcvg  24089  regamcl  24094  relgamcl  24095  divcnvlin  24513  clim2prod  24517  clim2div  24518  prodfdiv  24525  ntrivcvgtail  24529  ntrivcvgmullem  24530  fprodf1o  24573  prodss  24574  fprodss  24575  fprodser  24576  fprodcl2lem  24577  fprodmul  24585  fproddiv  24586  fprodefsum  24599  fprodn0  24604  iprodclim3  24607  iprodrecl  24609  iprodmul  24610  faclimlem2  24655  faclim2  24659  volsupnfl  25491  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  itg2gt0cn  25495  bddiblnc  25510  ftc1cnnclem  25513  ftc1cnnc  25514  clim1fr1  27050  climexp  27054  climinf  27055  climreeq  27062  dvsinexp  27063  wallispilem5  27141  wallispi  27142  stirlinglem8  27153  uhgrass  27512  usgrass  27539  usgraedg2  27550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-fv 5345
  Copyright terms: Public domain W3C validator