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

Theorem ffvelrnda 6021
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 6019 . 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 1767   -->wf 5584   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-id 4795  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-fv 5596
This theorem is referenced by:  ffvelrnd  6022  f1ocnvdm  6176  foeqcnvco  6191  f1oiso2  6236  suppssof1OLD  6543  ofco  6544  caofref  6550  caofinvl  6551  caofid0l  6552  caofid0r  6553  caofid1  6554  caofid2  6555  caofcom  6556  caofrss  6557  caofass  6558  caoftrn  6559  caofdi  6560  caofdir  6561  caonncan  6562  fnse  6900  suppssof1  6933  suppofss1d  6937  suppofss2d  6938  smofvon  7030  pw2f1olem  7621  mapxpen  7683  xpmapenlem  7684  supisoex  7932  wemappo  7974  wemapsolem  7975  cantnfp1lem1  8097  cantnfp1lem2  8098  cantnfp1lem3  8099  cantnflem1d  8107  cantnflem1  8108  cantnfp1lem1OLD  8123  cantnfp1lem2OLD  8124  cantnfp1lem3OLD  8125  cantnflem1dOLD  8130  cantnflem1OLD  8131  infxpenlem  8391  acndom  8432  acndom2  8435  iunfictbso  8495  ackbij2lem2  8620  cfsmolem  8650  infpssrlem3  8685  infpssrlem4  8686  isf32lem8  8740  isf34lem6  8760  axcc3  8818  axcclem  8837  canthnumlem  9026  ofsubeq0  10533  ofnegsub  10534  ofsubge0  10535  monoord2  12106  seqf1olem2  12115  seqf1o  12116  seqcoll  12478  wrdsymbcl  12525  ccatcl  12558  ccatco  12764  limsupgre  13267  limsupbnd1  13268  limsupbnd2  13269  rlimclim1  13331  rlimuni  13336  rlimresb  13351  o1co  13372  rlimcn1  13374  rlimo1  13402  clim2ser  13440  clim2ser2  13441  isermulc2  13443  iserle  13445  climserle  13448  isercolllem1  13450  isercolllem2  13451  isercoll  13453  caucvgrlem  13458  caucvgr  13461  iseraltlem1  13467  iseraltlem2  13468  iseraltlem3  13469  iseralt  13470  summolem3  13499  summolem2a  13500  fsumf1o  13508  sumss  13509  fsumss  13510  fsumcl2lem  13516  fsumadd  13524  isumclim3  13537  isummulc2  13540  isumrecl  13543  isumadd  13545  fsummulc2  13562  fsumrelem  13584  iserabs  13592  cvgcmp  13593  cvgcmpub  13594  cvgcmpce  13595  isumsplit  13615  climcndslem1  13624  climcndslem2  13625  climcnds  13626  supcvg  13630  mertens  13658  efcj  13689  rpnnen2lem5  13813  rpnnen2lem7  13815  rpnnen2lem8  13816  rpnnen2  13820  ruclem6  13829  ruclem8  13831  ruclem11  13834  ruclem12  13835  nn0seqcvgd  14058  alginv  14063  algcvg  14064  algcvga  14067  algfx  14068  eucalgcvga  14074  eulerthlem1  14170  eulerthlem2  14171  iserodd  14218  pcmptcl  14269  pcmpt  14270  prmreclem6  14298  1arithlem4  14303  vdwlem1  14358  vdwlem2  14359  vdwlem6  14363  vdwlem11  14368  0ram  14397  ramub1lem2  14404  ramcl  14406  imasvscafn  14792  imasvscaf  14794  cofucl  15115  cofulid  15117  funcres2b  15124  funcpropd  15127  ffthiso  15156  fuccocl  15191  fucidcl  15192  fuclid  15193  fucrid  15194  fucass  15195  fucsect  15199  fucinv  15200  invfuc  15201  fuciso  15202  natpropd  15203  fucpropd  15204  setcepi  15273  catcisolem  15291  prfcl  15330  prf1st  15331  prf2nd  15332  1st2ndprf  15333  evlfcl  15349  curfuncf  15365  hofcl  15386  yonedalem4c  15404  yonedainv  15408  yonffthlem  15409  prdsplusgcl  15770  prdsidlem  15771  prdsmndd  15772  pwsco1mhm  15820  pwsco2mhm  15821  gsumval2  15835  gsumwsubmcl  15838  gsumccat  15841  gsumwmhm  15845  grpinvcl  15905  mhmmulg  15984  prdsinvlem  15988  pwsinvg  15992  pwssub  15993  ghminv  16079  symgfv  16217  lactghmga  16234  symgtrinv  16303  psgnunilem5  16325  lsmhash  16529  efginvrel1  16552  efgsrel  16558  frgpuptf  16594  frgpuptinv  16595  frgpup3lem  16601  ghmplusg  16655  prdscmnd  16670  gsumval3eu  16710  gsumval3OLD  16711  gsumval3  16714  gsumzcl2  16718  gsumzf1o  16720  gsumzclOLD  16722  gsumzf1oOLD  16723  gsumzaddlem  16737  gsumzaddlemOLD  16739  gsumzsplit  16747  gsumzsplitOLD  16748  gsumconst  16757  gsumzmhm  16760  gsumzmhmOLD  16761  gsumzoppg  16770  gsumzoppgOLD  16771  gsumsub  16777  gsumsubOLD  16778  gsum2dlem1  16800  gsum2dlem2  16801  gsum2dOLD  16803  dmdprdd  16833  dprdff  16848  dprdfcntz  16851  dprdffOLD  16854  dprdfcntzOLD  16857  dprdfid  16859  dprdfinv  16861  dprdfadd  16862  dprdfsub  16863  dprdf11  16865  dprdfidOLD  16866  dprdfinvOLD  16868  dprdfaddOLD  16869  dprdfsubOLD  16870  dprdf11OLD  16872  dprdsubg  16873  dprdres  16877  dmdprdsplitlem  16886  dmdprdsplitlemOLD  16887  dprdcntz2  16888  dprd2da  16893  dmdprdsplit2lem  16896  ablfac1c  16924  ablfac1eu  16926  ablfaclem2  16939  ablfaclem3  16940  ablfac2  16942  prdsmulrcl  17061  prdsrngd  17062  isabvd  17269  abvcl  17273  abvge0  17274  srngcl  17304  lcomfsupOLD  17349  lcomfsupp  17350  prdsvscacl  17414  prdslmodd  17415  lmhmco  17489  lmhmvsca  17491  lmhmf1o  17492  pwssplit2  17506  pwssplit3  17507  rrgsupp  17738  rrgsuppOLD  17739  psrbagcon  17821  psrbaglefi  17822  psrbaglefiOLD  17823  psrbagconf1o  17825  gsumbagdiaglem  17826  psrass1lem  17828  psrlinv  17849  psrlidm  17855  psrlidmOLD  17856  psrridm  17857  psrridmOLD  17858  psrass1  17859  psrcom  17863  mplsubrglem  17899  mplsubrglemOLD  17900  mplmonmul  17925  mplcoe1  17926  mplcoe5lem  17929  mplcoe5  17930  mplcoe2OLD  17932  mplbas2  17933  mplbas2OLD  17934  mplcoe4  17967  evlslem2  17979  evlslem6  17980  evlslem6OLD  17981  evlslem1  17983  coe1fvalcl  18050  psrplusgpropd  18076  coe1subfv  18106  ply1sclcl  18126  ply1coe  18136  ply1coeOLD  18137  pf1mpf  18187  pf1ind  18190  gsumfsum  18280  zntoslem  18390  cygznlem3  18403  frgpcyg  18407  psgninv  18413  dsmmacl  18567  dsmmsubg  18569  dsmmlss  18570  frlmphl  18607  uvcresum  18619  frlmsslsp  18624  frlmsslspOLD  18625  frlmup1  18627  grpvrinv  18693  mhmvlin  18694  mdetleib2  18885  mdetf  18892  mdetcl  18893  mdetdiaglem  18895  mdetrlin  18899  mdetrsca  18900  mdetralt  18905  mdetunilem9  18917  mdetuni0  18918  madutpos  18939  madulid  18942  matunit  18975  m2pmfzmap  19043  pmatcollpw3fi1lem1  19082  pm2mp  19121  cpmadugsumlemF  19172  cpmadumatpoly  19179  cayhamlem2  19180  chcoeffeqlem  19181  cayhamlem4  19184  neiptopnei  19427  cnpcl  19543  lmss  19593  pnrmopn  19638  cnt1  19645  1stcelcls  19756  1stccnp  19757  1stckgen  19818  ptbasin  19841  ptpjpre2  19844  ptopn2  19848  dfac14  19882  ptcnplem  19885  ptcnp  19886  txcnmpt  19888  ptcn  19891  prdstps  19893  txcmplem2  19906  hauseqlcld  19910  txlm  19912  lmcn2  19913  qtopeu  19980  ordthmeolem  20065  xkocnv  20078  txflf  20270  ptcmplem3  20317  cnextfres  20331  symgtgp  20363  prdstmdd  20385  prdstgpd  20386  tsmssub  20414  tgptsmscls  20415  tsmssplit  20417  tsmsxplem1  20418  psmetxrge0  20580  imasf1obl  20754  prdsmslem1  20793  prdsxmslem1  20794  prdsxmslem2  20795  metcnp  20807  nmcl  20898  nrginvrcn  20963  nmocl  20990  nmoix  20999  nmoeq0  21006  metdseq0  21121  climcncf  21167  negfcncf  21186  evth  21222  evth2  21223  htpyco1  21241  reparphti  21260  nmhmcn  21366  cphnmcl  21406  lmmbrf  21464  cmetcaulem  21490  iscmet3lem2  21494  lmle  21503  caublcls  21510  bcthlem2  21527  bcthlem3  21528  bcthlem4  21529  rrxnm  21586  rrxcph  21587  rrxds  21588  rrxmval  21595  rrxmetlem  21597  rrxmet  21598  rrxdstprj1  21599  ivth2  21630  evthicc2  21635  cniccbdd  21636  ovolfsf  21646  ovolsf  21647  ovollb2lem  21662  ovolctb  21664  ovolunlem1a  21670  ovolunlem1  21671  ovoliunlem1  21676  ovoliunlem2  21677  ovoliun  21679  ovoliunnul  21681  ovolicc2lem1  21691  ovolicc2lem2  21692  ovolicc2lem4  21694  ovolicc2lem5  21695  voliunlem2  21724  voliunlem3  21725  iunmbl2  21730  ioombl1lem4  21734  ovolfs2  21743  uniiccdif  21750  uniioombllem2a  21754  uniioombllem2  21755  uniioombllem3  21757  uniioombllem6  21760  volivth  21779  vitalilem2  21781  vitalilem4  21783  vitalilem5  21784  mbfmulc2lem  21817  mbfmulc2re  21818  mbfmax  21819  mbfposb  21823  mbfimaopnlem  21825  mbfaddlem  21830  mbfsup  21834  mbflimlem  21837  mbflim  21838  i1fmulclem  21872  itg1mulc  21874  i1fpos  21876  itg1lea  21882  itg1climres  21884  mbfi1fseqlem3  21887  mbfi1fseqlem4  21888  mbfi1fseqlem5  21889  mbfi1fseqlem6  21890  mbfi1flimlem  21892  mbfi1flim  21893  mbfmullem2  21894  itg2uba  21913  itg2mulclem  21916  itg2mulc  21917  itg2monolem1  21920  itg2mono  21923  itg2i1fseqle  21924  itg2i1fseq  21925  itg2i1fseq2  21926  itg2i1fseq3  21927  itg2addlem  21928  itg2gt0  21930  itg2cnlem1  21931  itg2cnlem2  21932  itg2cn  21933  i1fibl  21977  itgitg1  21978  bddmulibl  22008  bddibl  22009  ellimc2  22044  limcres  22053  dvcnp2  22086  dvnf  22093  dvnbss  22094  dvnadd  22095  dvcmulf  22111  dvcof  22114  dvcnv  22141  rolle  22154  cmvth  22155  mvth  22156  dvlip  22157  dvlipcn  22158  dveq0  22164  dv11cn  22165  dvgt0lem1  22166  dvivthlem1  22172  dvivth  22174  dvne0  22175  lhop1lem  22177  lhop1  22178  lhop2  22179  lhop  22180  dvcnvre  22183  ftc1lem1  22199  ftc1lem4  22203  ftc1lem6  22205  ftc2  22208  itgsubst  22213  tdeglem4  22221  mdegleb  22227  mdegnn0cl  22234  mdegaddle  22237  mdegle0  22240  mdegmullem  22241  deg1sclle  22276  deg1scl  22277  fta1glem2  22330  elply2  22356  plypf1  22372  plyaddlem1  22373  plymullem1  22374  coeeulem  22384  coeidlem  22397  coeid3  22400  plyco  22401  coemulc  22414  dgrcolem1  22432  dgrcolem2  22433  dgrco  22434  coecj  22437  ofmulrt  22440  dvply2g  22443  plydivlem3  22453  plydiveu  22456  plyrem  22463  vieta1  22470  elqaalem1  22477  elqaalem3  22479  aannenlem1  22486  aannenlem2  22487  taylthlem1  22530  taylthlem2  22531  ulmclm  22544  ulmcaulem  22551  ulmcau  22552  ulmcn  22556  ulmdvlem1  22557  ulmdvlem3  22559  mtest  22561  mtestbdd  22562  mbfulm  22563  iblulm  22564  itgulm  22565  radcnvlem1  22570  radcnvlem2  22571  radcnvlem3  22572  radcnv0  22573  radcnvlt2  22576  dvradcnv  22578  pserulm  22579  psercn2  22580  pserdvlem2  22585  abelthlem1  22588  abelthlem3  22590  abelthlem4  22591  abelthlem5  22592  abelthlem6  22593  abelthlem7  22595  abelthlem8  22596  abelthlem9  22597  abelth  22598  atantayl  23024  leibpi  23029  o1cxp  23060  jensenlem1  23072  jensenlem2  23073  jensen  23074  amgmlem  23075  ftalem4  23105  basellem4  23113  basellem7  23116  basellem9  23118  muinv  23225  dchrmulcl  23280  dchrmulid2  23283  dchrinvcl  23284  dchrinv  23292  dchrptlem2  23296  dchrptlem3  23297  bposlem5  23319  lgsfle1  23336  lgsdchrval  23378  dchrisumlem1  23430  dchrisumlem3  23432  dchrmusum2  23435  dchrisum0re  23454  dchrisum0lem1b  23456  dchrisum0lem2a  23458  f1otrg  23878  fveere  23908  axcontlem5  23975  uhgrass  24010  umgrass  24023  umgran0  24024  umgrale  24025  usgrass  24065  usgraedg2  24079  usgfidegfi  24614  eupap1  24680  numclwlk2lem2f1o  24810  ghgrp  25074  nvcl  25266  nvlmle  25306  blometi  25422  ubthlem1  25490  ubthlem2  25491  minvecolem3  25496  minvecolem4  25500  htthlem  25538  hlimadd  25814  occllem  25925  chscllem1  26259  chscllem2  26260  chscllem4  26262  unopnorm  26540  cnvunop  26541  unopadj  26542  unoplin  26543  hmopre  26546  adjcl  26555  adj2  26557  hmoplin  26565  bracl  26572  lnopmul  26590  homco2  26600  hmopco  26646  adjlnop  26709  adjmul  26715  adjadd  26716  kbass5  26743  leopsq  26752  hmopidmchi  26774  hstcl  26840  iunrdx  27132  disjrdx  27151  ofresid  27183  xppreima2  27188  ofoprabco  27205  isoun  27220  fpwrelmap  27256  rhmdvdsr  27499  tpr2rico  27558  rge0scvg  27595  fsumcvg4  27596  lmxrge0  27598  lmdvg  27599  qqhucn  27637  indsum  27704  indpreima  27706  esumf1o  27729  esumpcvgval  27752  ofcf  27770  ofcfval4  27772  measvxrge0  27844  meascnbl  27858  volmeas  27871  mbfmco2  27904  eulerpartlems  27967  eulerpartlemgc  27969  eulerpartlemd  27973  eulerpartgbij  27979  eulerpartlemgvv  27983  rrvsum  28061  dstfrvunirn  28081  gsumncl  28160  plymul02  28171  signsply0  28176  lgamgulmlem6  28244  lgamgulm2  28246  gamcvg  28266  regamcl  28271  relgamcl  28272  derangenlem  28283  subfacp1lem4  28295  subfacp1lem5  28296  erdszelem9  28311  ptpcon  28346  cvxscon  28356  cvmliftmolem2  28395  cvmliftlem15  28411  cvmlift2lem3  28418  cvmlift3lem4  28435  cvmlift3lem5  28436  cvmlift3lem8  28439  divcnvlin  28623  clim2prod  28627  clim2div  28628  prodfdiv  28635  ntrivcvgtail  28639  ntrivcvgmullem  28640  prodmolem3  28670  prodmolem2a  28671  fprodf1o  28683  prodss  28684  fprodss  28685  fprodser  28686  fprodcl2lem  28687  fprodmul  28695  fproddiv  28696  fprodefsum  28709  fprodn0  28714  iprodclim3  28724  iprodrecl  28726  iprodmul  28727  iprodefisumlem  28728  faclimlem2  28774  faclim2  28778  ptrest  29653  heicant  29654  mblfinlem2  29657  volsupnfl  29664  itg2addnclem  29671  itg2addnclem2  29672  itg2addnclem3  29673  itg2addnc  29674  itg2gt0cn  29675  bddiblnc  29690  ftc1cnnclem  29693  ftc1cnnc  29694  ftc1anclem3  29697  ftc1anclem4  29698  ftc1anclem5  29699  ftc1anclem6  29700  ftc1anclem7  29701  ftc1anclem8  29702  ftc1anc  29703  ftc2nc  29704  neibastop1  29808  neibastop2lem  29809  filnetlem4  29830  sdclem2  29866  lmclim2  29882  geomcau  29883  ismtybndlem  29933  heiborlem3  29940  heiborlem5  29942  heiborlem6  29943  heiborlem8  29945  heibor  29948  bfplem1  29949  bfplem2  29950  rrnmet  29956  rrndstprj1  29957  rrndstprj2  29958  rrncmslem  29959  ismrer1  29965  ghomdiv  29977  grpokerinj  29978  rngohomcl  30001  ismrcd2  30263  mzpsubst  30313  fphpdo  30383  wepwsolem  30619  hbt  30711  mendlmod  30775  mendassa  30776  caofcan  30856  ofmul12  30858  fnvinran  30995  rfcnnnub  31017  fmuldfeq  31161  clim1fr1  31171  climexp  31175  climinf  31176  climreeq  31183  mullimc  31186  ellimcabssub0  31187  mullimcf  31193  limcrecl  31199  sumnnodd  31200  limsupre  31211  neglimc  31217  addlimc  31218  0ellimcdiv  31219  limclner  31221  sinmulcos  31229  mulcncff  31234  subcncff  31246  addcncff  31251  icccncfext  31254  cncficcgt0  31255  divcncff  31258  cncfiooicclem1  31260  dvsinexp  31266  dvsubf  31270  dvdivf  31280  dvbdfbdioolem2  31287  ioodvbdlimc1lem1  31289  iblcncfioo  31324  itgiccshift  31326  stoweidlem20  31348  wallispilem5  31397  wallispi  31398  stirlinglem8  31409  fourierdlem12  31447  fourierdlem15  31450  fourierdlem16  31451  fourierdlem20  31455  fourierdlem22  31457  fourierdlem34  31469  fourierdlem39  31474  fourierdlem41  31476  fourierdlem45  31480  fourierdlem48  31483  fourierdlem49  31484  fourierdlem50  31485  fourierdlem51  31486  fourierdlem54  31489  fourierdlem56  31491  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem63  31498  fourierdlem70  31505  fourierdlem72  31507  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem81  31516  fourierdlem82  31517  fourierdlem87  31522  fourierdlem88  31523  fourierdlem92  31527  fourierdlem95  31530  fourierdlem97  31532  fourierdlem101  31536  fourierdlem102  31537  fourierdlem103  31538  fourierdlem104  31539  fourierdlem111  31546  fourierdlem114  31549  fouriersw  31560  uhgss  31864  lincresunit3  32181  lautcl  34901
  Copyright terms: Public domain W3C validator