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

Theorem ffvelrnda 5838
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 5836 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 471 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   -->wf 5409   ` cfv 5413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-id 4631  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-fv 5421
This theorem is referenced by:  ffvelrnd  5839  f1ocnvdm  5984  foeqcnvco  5993  f1oiso2  6038  suppssof1OLD  6334  ofco  6335  caofref  6341  caofinvl  6342  caofid0l  6343  caofid0r  6344  caofid1  6345  caofid2  6346  caofcom  6347  caofrss  6348  caofass  6349  caoftrn  6350  caofdi  6351  caofdir  6352  caonncan  6353  fnse  6684  suppssof1  6717  suppofss1d  6721  suppofss2d  6722  smofvon  6812  pw2f1olem  7407  mapxpen  7469  xpmapenlem  7470  supisoex  7713  wemappo  7755  wemapsolem  7756  cantnfp1lem1  7878  cantnfp1lem2  7879  cantnfp1lem3  7880  cantnflem1d  7888  cantnflem1  7889  cantnfp1lem1OLD  7904  cantnfp1lem2OLD  7905  cantnfp1lem3OLD  7906  cantnflem1dOLD  7911  cantnflem1OLD  7912  infxpenlem  8172  acndom  8213  acndom2  8216  iunfictbso  8276  ackbij2lem2  8401  cfsmolem  8431  infpssrlem3  8466  infpssrlem4  8467  isf32lem8  8521  isf34lem6  8541  axcc3  8599  axcclem  8618  canthnumlem  8807  ofsubeq0  10311  ofnegsub  10312  ofsubge0  10313  monoord2  11829  seqf1olem2  11838  seqf1o  11839  seqcoll  12208  wrdsymbcl  12238  ccatcl  12266  ccatco  12455  limsupgre  12951  limsupbnd1  12952  limsupbnd2  12953  rlimclim1  13015  rlimuni  13020  rlimresb  13035  o1co  13056  rlimcn1  13058  rlimo1  13086  clim2ser  13124  clim2ser2  13125  isermulc2  13127  iserle  13129  climserle  13132  isercolllem1  13134  isercolllem2  13135  isercoll  13137  caucvgrlem  13142  caucvgr  13145  iseraltlem1  13151  iseraltlem2  13152  iseraltlem3  13153  iseralt  13154  summolem3  13183  summolem2a  13184  fsumf1o  13192  sumss  13193  fsumss  13194  fsumcl2lem  13200  fsumadd  13207  isumclim3  13218  isummulc2  13221  isumrecl  13224  isumadd  13226  fsummulc2  13243  fsumrelem  13262  iserabs  13270  cvgcmp  13271  cvgcmpub  13272  cvgcmpce  13273  isumsplit  13295  climcndslem1  13304  climcndslem2  13305  climcnds  13306  supcvg  13310  mertens  13338  efcj  13369  rpnnen2lem5  13493  rpnnen2lem7  13495  rpnnen2lem8  13496  rpnnen2  13500  ruclem6  13509  ruclem8  13511  ruclem11  13514  ruclem12  13515  nn0seqcvgd  13737  alginv  13742  algcvg  13743  algcvga  13746  algfx  13747  eucalgcvga  13753  eulerthlem1  13848  eulerthlem2  13849  iserodd  13894  pcmptcl  13945  pcmpt  13946  prmreclem6  13974  1arithlem4  13979  vdwlem1  14034  vdwlem2  14035  vdwlem6  14039  vdwlem11  14044  0ram  14073  ramub1lem2  14080  ramcl  14082  imasvscafn  14467  imasvscaf  14469  cofucl  14790  cofulid  14792  funcres2b  14799  funcpropd  14802  ffthiso  14831  fuccocl  14866  fucidcl  14867  fuclid  14868  fucrid  14869  fucass  14870  fucsect  14874  fucinv  14875  invfuc  14876  fuciso  14877  natpropd  14878  fucpropd  14879  setcepi  14948  catcisolem  14966  prfcl  15005  prf1st  15006  prf2nd  15007  1st2ndprf  15008  evlfcl  15024  curfuncf  15040  hofcl  15061  yonedalem4c  15079  yonedainv  15083  yonffthlem  15084  prdsplusgcl  15444  prdsidlem  15445  prdsmndd  15446  pwsco1mhm  15489  pwsco2mhm  15490  gsumval2  15504  gsumwsubmcl  15507  gsumccat  15510  gsumwmhm  15514  grpinvcl  15574  mhmmulg  15650  prdsinvlem  15654  pwsinvg  15658  pwssub  15659  ghminv  15745  symgfv  15883  lactghmga  15900  symgtrinv  15969  psgnunilem5  15991  lsmhash  16193  efginvrel1  16216  efgsrel  16222  frgpuptf  16258  frgpuptinv  16259  frgpup3lem  16265  ghmplusg  16319  prdscmnd  16334  gsumval3eu  16372  gsumval3OLD  16373  gsumval3  16376  gsumzcl2  16380  gsumzf1o  16382  gsumzclOLD  16384  gsumzf1oOLD  16385  gsumzaddlem  16399  gsumzaddlemOLD  16401  gsumzsplit  16409  gsumzsplitOLD  16410  gsumconst  16417  gsumzmhm  16420  gsumzmhmOLD  16421  gsumzoppg  16430  gsumzoppgOLD  16431  gsumsub  16437  gsumsubOLD  16438  gsum2dlem1  16451  gsum2dlem2  16452  gsum2dOLD  16454  dmdprdd  16471  dprdff  16486  dprdfcntz  16489  dprdffOLD  16492  dprdfcntzOLD  16495  dprdfid  16497  dprdfinv  16499  dprdfadd  16500  dprdfsub  16501  dprdf11  16503  dprdfidOLD  16504  dprdfinvOLD  16506  dprdfaddOLD  16507  dprdfsubOLD  16508  dprdf11OLD  16510  dprdsubg  16511  dprdres  16515  dmdprdsplitlem  16524  dmdprdsplitlemOLD  16525  dprdcntz2  16526  dprd2da  16531  dmdprdsplit2lem  16534  ablfac1c  16562  ablfac1eu  16564  ablfaclem2  16577  ablfaclem3  16578  ablfac2  16580  prdsmulrcl  16693  prdsrngd  16694  isabvd  16885  abvcl  16889  abvge0  16890  srngcl  16920  lcomfsupOLD  16964  lcomfsupp  16965  prdsvscacl  17029  prdslmodd  17030  lmhmco  17104  lmhmvsca  17106  lmhmf1o  17107  pwssplit2  17121  pwssplit3  17122  rrgsupp  17342  rrgsuppOLD  17343  psrbagcon  17420  psrbaglefi  17421  psrbaglefiOLD  17422  psrbagconf1o  17424  gsumbagdiaglem  17425  psrass1lem  17427  psrlinv  17448  psrlidm  17454  psrlidmOLD  17455  psrridm  17456  psrridmOLD  17457  psrass1  17458  psrcom  17461  mplsubrglem  17497  mplsubrglemOLD  17498  mplmonmul  17523  mplcoe1  17524  mplcoe5lem  17527  mplcoe5  17528  mplcoe2OLD  17530  mplbas2  17531  mplbas2OLD  17532  mplcoe4  17565  evlslem2  17577  evlslem6  17578  evlslem6OLD  17579  evlslem1  17581  psrplusgpropd  17670  coe1subfv  17700  ply1coe  17726  ply1coeOLD  17727  pf1mpf  17766  pf1ind  17769  gsumfsum  17859  zntoslem  17969  cygznlem3  17982  frgpcyg  17986  psgninv  17992  dsmmacl  18146  dsmmsubg  18148  dsmmlss  18149  frlmphl  18186  uvcresum  18198  frlmsslsp  18203  frlmsslspOLD  18204  frlmup1  18206  grpvrinv  18276  mhmvlin  18277  mdetleib2  18379  mdetf  18386  mdetcl  18387  mdet1  18388  mdetrlin  18389  mdetrsca  18390  mdetralt  18394  mdetunilem9  18406  mdetuni0  18407  madutpos  18428  madulid  18431  matunit  18464  neiptopnei  18716  cnpcl  18832  lmss  18882  pnrmopn  18927  cnt1  18934  1stcelcls  19045  1stccnp  19046  1stckgen  19107  ptbasin  19130  ptpjpre2  19133  ptopn2  19137  dfac14  19171  ptcnplem  19174  ptcnp  19175  txcnmpt  19177  ptcn  19180  prdstps  19182  txcmplem2  19195  hauseqlcld  19199  txlm  19201  lmcn2  19202  qtopeu  19269  ordthmeolem  19354  xkocnv  19367  txflf  19559  ptcmplem3  19606  cnextfres  19620  symgtgp  19652  prdstmdd  19674  prdstgpd  19675  tsmssub  19703  tgptsmscls  19704  tsmssplit  19706  tsmsxplem1  19707  psmetxrge0  19869  imasf1obl  20043  prdsmslem1  20082  prdsxmslem1  20083  prdsxmslem2  20084  metcnp  20096  nmcl  20187  nrginvrcn  20252  nmocl  20279  nmoix  20288  nmoeq0  20295  metdseq0  20410  climcncf  20456  negfcncf  20475  evth  20511  evth2  20512  htpyco1  20530  reparphti  20549  nmhmcn  20655  cphnmcl  20695  lmmbrf  20753  cmetcaulem  20779  iscmet3lem2  20783  lmle  20792  caublcls  20799  bcthlem2  20816  bcthlem3  20817  bcthlem4  20818  rrxnm  20875  rrxcph  20876  rrxds  20877  rrxmval  20884  rrxmetlem  20886  rrxmet  20887  rrxdstprj1  20888  ivth2  20919  evthicc2  20924  cniccbdd  20925  ovolfsf  20935  ovolsf  20936  ovollb2lem  20951  ovolctb  20953  ovolunlem1a  20959  ovolunlem1  20960  ovoliunlem1  20965  ovoliunlem2  20966  ovoliun  20968  ovoliunnul  20970  ovolicc2lem1  20980  ovolicc2lem2  20981  ovolicc2lem4  20983  ovolicc2lem5  20984  voliunlem2  21012  voliunlem3  21013  iunmbl2  21018  ioombl1lem4  21022  ovolfs2  21031  uniiccdif  21038  uniioombllem2a  21042  uniioombllem2  21043  uniioombllem3  21045  uniioombllem6  21048  volivth  21067  vitalilem2  21069  vitalilem4  21071  vitalilem5  21072  mbfmulc2lem  21105  mbfmulc2re  21106  mbfmax  21107  mbfposb  21111  mbfimaopnlem  21113  mbfaddlem  21118  mbfsup  21122  mbflimlem  21125  mbflim  21126  i1fmulclem  21160  itg1mulc  21162  i1fpos  21164  itg1lea  21170  itg1climres  21172  mbfi1fseqlem3  21175  mbfi1fseqlem4  21176  mbfi1fseqlem5  21177  mbfi1fseqlem6  21178  mbfi1flimlem  21180  mbfi1flim  21181  mbfmullem2  21182  itg2uba  21201  itg2mulclem  21204  itg2mulc  21205  itg2monolem1  21208  itg2mono  21211  itg2i1fseqle  21212  itg2i1fseq  21213  itg2i1fseq2  21214  itg2i1fseq3  21215  itg2addlem  21216  itg2gt0  21218  itg2cnlem1  21219  itg2cnlem2  21220  itg2cn  21221  i1fibl  21265  itgitg1  21266  bddmulibl  21296  bddibl  21297  ellimc2  21332  limcres  21341  dvcnp2  21374  dvnf  21381  dvnbss  21382  dvnadd  21383  dvcmulf  21399  dvcof  21402  dvcnv  21429  rolle  21442  cmvth  21443  mvth  21444  dvlip  21445  dvlipcn  21446  dveq0  21452  dv11cn  21453  dvgt0lem1  21454  dvivthlem1  21460  dvivth  21462  dvne0  21463  lhop1lem  21465  lhop1  21466  lhop2  21467  lhop  21468  dvcnvre  21471  ftc1lem1  21487  ftc1lem4  21491  ftc1lem6  21493  ftc2  21496  itgsubst  21501  tdeglem4  21509  mdegleb  21515  mdegnn0cl  21522  mdegaddle  21525  mdegle0  21528  mdegmullem  21529  deg1sclle  21564  deg1scl  21565  fta1glem2  21618  elply2  21644  plypf1  21660  plyaddlem1  21661  plymullem1  21662  coeeulem  21672  coeidlem  21685  coeid3  21688  plyco  21689  coemulc  21702  dgrcolem1  21720  dgrcolem2  21721  dgrco  21722  coecj  21725  ofmulrt  21728  dvply2g  21731  plydivlem3  21741  plydiveu  21744  plyrem  21751  vieta1  21758  elqaalem1  21765  elqaalem3  21767  aannenlem1  21774  aannenlem2  21775  taylthlem1  21818  taylthlem2  21819  ulmclm  21832  ulmcaulem  21839  ulmcau  21840  ulmcn  21844  ulmdvlem1  21845  ulmdvlem3  21847  mtest  21849  mtestbdd  21850  mbfulm  21851  iblulm  21852  itgulm  21853  radcnvlem1  21858  radcnvlem2  21859  radcnvlem3  21860  radcnv0  21861  radcnvlt2  21864  dvradcnv  21866  pserulm  21867  psercn2  21868  pserdvlem2  21873  abelthlem1  21876  abelthlem3  21878  abelthlem4  21879  abelthlem5  21880  abelthlem6  21881  abelthlem7  21883  abelthlem8  21884  abelthlem9  21885  abelth  21886  atantayl  22312  leibpi  22317  o1cxp  22348  jensenlem1  22360  jensenlem2  22361  jensen  22362  amgmlem  22363  ftalem4  22393  basellem4  22401  basellem7  22404  basellem9  22406  muinv  22513  dchrmulcl  22568  dchrmulid2  22571  dchrinvcl  22572  dchrinv  22580  dchrptlem2  22584  dchrptlem3  22585  bposlem5  22607  lgsfle1  22624  lgsdchrval  22666  dchrisumlem1  22718  dchrisumlem3  22720  dchrmusum2  22723  dchrisum0re  22742  dchrisum0lem1b  22744  dchrisum0lem2a  22746  f1otrg  23085  fveere  23115  axcontlem5  23182  uhgrass  23208  umgrass  23221  umgran0  23222  umgrale  23223  usgrass  23251  usgraedg2  23262  eupap1  23565  ghgrp  23823  nvcl  24015  nvlmle  24055  blometi  24171  ubthlem1  24239  ubthlem2  24240  minvecolem3  24245  minvecolem4  24249  htthlem  24287  hlimadd  24563  occllem  24674  chscllem1  25008  chscllem2  25009  chscllem4  25011  unopnorm  25289  cnvunop  25290  unopadj  25291  unoplin  25292  hmopre  25295  adjcl  25304  adj2  25306  hmoplin  25314  bracl  25321  lnopmul  25339  homco2  25349  hmopco  25395  adjlnop  25458  adjmul  25464  adjadd  25465  kbass5  25492  leopsq  25501  hmopidmchi  25523  hstcl  25589  iunrdx  25882  disjrdx  25901  ofresid  25928  xppreima2  25933  ofoprabco  25950  isoun  25965  fpwrelmap  26001  rhmdvdsr  26254  tpr2rico  26311  rge0scvg  26348  fsumcvg4  26349  lmxrge0  26351  lmdvg  26352  qqhucn  26390  indsum  26448  indpreima  26450  esumf1o  26473  esumpcvgval  26496  ofcf  26514  ofcfval4  26516  measvxrge0  26588  meascnbl  26602  volmeas  26616  mbfmco2  26649  eulerpartlems  26712  eulerpartlemgc  26714  eulerpartlemd  26718  eulerpartgbij  26724  eulerpartlemgvv  26728  rrvsum  26806  dstfrvunirn  26826  gsumncl  26905  plymul02  26916  signsply0  26921  lgamgulmlem6  26989  lgamgulm2  26991  gamcvg  27011  regamcl  27016  relgamcl  27017  derangenlem  27028  subfacp1lem4  27040  subfacp1lem5  27041  erdszelem9  27056  ptpcon  27091  cvxscon  27101  cvmliftmolem2  27140  cvmliftlem15  27156  cvmlift2lem3  27163  cvmlift3lem4  27180  cvmlift3lem5  27181  cvmlift3lem8  27184  divcnvlin  27368  clim2prod  27372  clim2div  27373  prodfdiv  27380  ntrivcvgtail  27384  ntrivcvgmullem  27385  prodmolem3  27415  prodmolem2a  27416  fprodf1o  27428  prodss  27429  fprodss  27430  fprodser  27431  fprodcl2lem  27432  fprodmul  27440  fproddiv  27441  fprodefsum  27454  fprodn0  27459  iprodclim3  27469  iprodrecl  27471  iprodmul  27472  iprodefisumlem  27473  faclimlem2  27519  faclim2  27523  ptrest  28396  heicant  28397  mblfinlem2  28400  volsupnfl  28407  itg2addnclem  28414  itg2addnclem2  28415  itg2addnclem3  28416  itg2addnc  28417  itg2gt0cn  28418  bddiblnc  28433  ftc1cnnclem  28436  ftc1cnnc  28437  ftc1anclem3  28440  ftc1anclem4  28441  ftc1anclem5  28442  ftc1anclem6  28443  ftc1anclem7  28444  ftc1anclem8  28445  ftc1anc  28446  ftc2nc  28447  neibastop1  28551  neibastop2lem  28552  filnetlem4  28573  sdclem2  28609  lmclim2  28625  geomcau  28626  ismtybndlem  28676  heiborlem3  28683  heiborlem5  28685  heiborlem6  28686  heiborlem8  28688  heibor  28691  bfplem1  28692  bfplem2  28693  rrnmet  28699  rrndstprj1  28700  rrndstprj2  28701  rrncmslem  28702  ismrer1  28708  ghomdiv  28720  grpokerinj  28721  rngohomcl  28744  ismrcd2  29006  mzpsubst  29056  fphpdo  29127  wepwsolem  29365  hbt  29457  mendlmod  29521  mendassa  29522  caofcan  29568  ofmul12  29570  fnvinran  29707  rfcnnnub  29729  fmuldfeq  29735  clim1fr1  29745  climexp  29749  climinf  29750  climreeq  29757  dvsinexp  29758  stoweidlem20  29786  wallispilem5  29835  wallispi  29836  stirlinglem8  29847  usgfidegfi  30498  numclwlk2lem2f1o  30669  coe1fvalcl  30796  mdetdiaglem  30866  lincresunit3  30946  lautcl  33624
  Copyright terms: Public domain W3C validator