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

Theorem ffvelrnda 6016
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 6014 . 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 1804   -->wf 5574   ` cfv 5578
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-id 4785  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586
This theorem is referenced by:  ffvelrnd  6017  f1ocnvdm  6173  foeqcnvco  6188  f1oiso2  6233  suppssof1OLD  6544  ofco  6545  caofref  6551  caofinvl  6552  caofid0l  6553  caofid0r  6554  caofid1  6555  caofid2  6556  caofcom  6557  caofrss  6558  caofass  6559  caoftrn  6560  caofdi  6561  caofdir  6562  caonncan  6563  fnse  6902  suppssof1  6935  suppofss1d  6939  suppofss2d  6940  smofvon  7032  pw2f1olem  7623  mapxpen  7685  xpmapenlem  7686  supisoex  7935  wemappo  7977  wemapsolem  7978  cantnfp1lem1  8100  cantnfp1lem2  8101  cantnfp1lem3  8102  cantnflem1d  8110  cantnflem1  8111  cantnfp1lem1OLD  8126  cantnfp1lem2OLD  8127  cantnfp1lem3OLD  8128  cantnflem1dOLD  8133  cantnflem1OLD  8134  infxpenlem  8394  acndom  8435  acndom2  8438  iunfictbso  8498  ackbij2lem2  8623  cfsmolem  8653  infpssrlem3  8688  infpssrlem4  8689  isf32lem8  8743  isf34lem6  8763  axcc3  8821  axcclem  8840  canthnumlem  9029  ofsubeq0  10540  ofnegsub  10541  ofsubge0  10542  monoord2  12120  seqf1olem2  12129  seqf1o  12130  seqcoll  12494  wrdsymbcl  12541  ccatcl  12575  ccatco  12783  limsupgre  13286  limsupbnd1  13287  limsupbnd2  13288  rlimclim1  13350  rlimuni  13355  rlimresb  13370  o1co  13391  rlimcn1  13393  rlimo1  13421  clim2ser  13459  clim2ser2  13460  isermulc2  13462  iserle  13464  climserle  13467  isercolllem1  13469  isercolllem2  13470  isercoll  13472  caucvgrlem  13477  caucvgr  13480  iseraltlem1  13486  iseraltlem2  13487  iseraltlem3  13488  iseralt  13489  summolem3  13518  summolem2a  13519  fsumf1o  13527  sumss  13528  fsumss  13529  fsumcl2lem  13535  fsumadd  13543  isumclim3  13556  isummulc2  13559  isumrecl  13562  isumadd  13564  fsummulc2  13581  fsumrelem  13603  iserabs  13611  cvgcmp  13612  cvgcmpub  13613  cvgcmpce  13614  isumsplit  13634  climcndslem1  13643  climcndslem2  13644  climcnds  13645  supcvg  13649  mertens  13677  clim2prod  13679  clim2div  13680  prodfdiv  13687  ntrivcvgtail  13691  ntrivcvgmullem  13692  prodmolem3  13722  prodmolem2a  13723  fprodf1o  13735  prodss  13736  fprodss  13737  fprodser  13738  fprodcl2lem  13739  fprodmul  13747  fproddiv  13748  fprodn0  13765  iprodclim3  13775  iprodrecl  13777  iprodmul  13778  efcj  13809  fprodefsum  13812  rpnnen2lem5  13934  rpnnen2lem7  13936  rpnnen2lem8  13937  rpnnen2  13941  ruclem6  13950  ruclem8  13952  ruclem11  13955  ruclem12  13956  nn0seqcvgd  14181  alginv  14186  algcvg  14187  algcvga  14190  algfx  14191  eucalgcvga  14197  eulerthlem1  14293  eulerthlem2  14294  iserodd  14341  pcmptcl  14392  pcmpt  14393  prmreclem6  14421  1arithlem4  14426  vdwlem1  14481  vdwlem2  14482  vdwlem6  14486  vdwlem11  14491  0ram  14520  ramub1lem2  14527  ramcl  14529  imasvscafn  14916  imasvscaf  14918  cofucl  15236  cofulid  15238  funcres2b  15245  funcpropd  15248  ffthiso  15277  fuccocl  15312  fucidcl  15313  fuclid  15314  fucrid  15315  fucass  15316  fucsect  15320  fucinv  15321  invfuc  15322  fuciso  15323  natpropd  15324  fucpropd  15325  setcepi  15394  catcisolem  15412  prfcl  15451  prf1st  15452  prf2nd  15453  1st2ndprf  15454  evlfcl  15470  curfuncf  15486  hofcl  15507  yonedalem4c  15525  yonedainv  15529  yonffthlem  15530  gsumval2  15886  prdsplusgcl  15930  prdsidlem  15931  prdsmndd  15932  pwsco1mhm  15980  pwsco2mhm  15981  gsumwsubmcl  15985  gsumccat  15988  gsumwmhm  15992  grpinvcl  16074  mhmmulg  16153  prdsinvlem  16157  pwsinvg  16161  pwssub  16162  ghminv  16253  symgfv  16391  lactghmga  16408  symgtrinv  16476  psgnunilem5  16498  lsmhash  16702  efginvrel1  16725  efgsrel  16731  frgpuptf  16767  frgpuptinv  16768  frgpup3lem  16774  ghmplusg  16831  prdscmnd  16846  gsumval3eu  16886  gsumval3OLD  16887  gsumval3  16890  gsumzcl2  16894  gsumzf1o  16896  gsumzclOLD  16898  gsumzf1oOLD  16899  gsumzaddlem  16913  gsumzaddlemOLD  16915  gsumzsplit  16923  gsumzsplitOLD  16924  gsumconst  16933  gsumzmhm  16936  gsumzmhmOLD  16937  gsumzoppg  16946  gsumzoppgOLD  16947  gsumsub  16953  gsumsubOLD  16954  gsum2dlem1  16976  gsum2dlem2  16977  gsum2dOLD  16979  dmdprdd  17009  dprdff  17025  dprdfcntz  17028  dprdffOLD  17031  dprdfcntzOLD  17034  dprdfid  17036  dprdfinv  17038  dprdfadd  17039  dprdfsub  17040  dprdf11  17042  dprdfidOLD  17043  dprdfinvOLD  17045  dprdfaddOLD  17046  dprdfsubOLD  17047  dprdf11OLD  17049  dprdsubg  17050  dprdres  17054  dprdf1o  17058  dmdprdsplitlem  17063  dmdprdsplitlemOLD  17064  dprdcntz2  17065  dprd2da  17070  dmdprdsplit2lem  17073  ablfac1c  17101  ablfac1eu  17103  ablfaclem2  17116  ablfaclem3  17117  ablfac2  17119  prdsmulrcl  17239  prdsringd  17240  isabvd  17448  abvcl  17452  abvge0  17453  srngcl  17483  lcomfsupOLD  17528  lcomfsupp  17529  prdsvscacl  17593  prdslmodd  17594  lmhmco  17668  lmhmvsca  17670  lmhmf1o  17671  pwssplit2  17685  pwssplit3  17686  rrgsupp  17918  rrgsuppOLD  17919  psrbagcon  18001  psrbaglefi  18002  psrbaglefiOLD  18003  psrbagconf1o  18005  gsumbagdiaglem  18006  psrass1lem  18008  psrlinv  18029  psrlidm  18035  psrlidmOLD  18036  psrridm  18037  psrridmOLD  18038  psrass1  18039  psrcom  18043  mplsubrglem  18079  mplsubrglemOLD  18080  mplmonmul  18105  mplcoe1  18106  mplcoe5lem  18109  mplcoe5  18110  mplcoe2OLD  18112  mplbas2  18113  mplbas2OLD  18114  mplcoe4  18147  evlslem2  18159  evlslem6  18160  evlslem6OLD  18161  evlslem1  18163  coe1fvalcl  18230  psrplusgpropd  18256  coe1subfv  18286  ply1sclcl  18306  ply1coe  18316  ply1coeOLD  18317  pf1mpf  18367  pf1ind  18370  gsumfsum  18463  zntoslem  18573  cygznlem3  18586  frgpcyg  18590  psgninv  18596  dsmmacl  18750  dsmmsubg  18752  dsmmlss  18753  frlmphl  18790  uvcresum  18802  frlmsslsp  18807  frlmsslspOLD  18808  frlmup1  18810  grpvrinv  18876  mhmvlin  18877  mdetleib2  19068  mdetf  19075  mdetcl  19076  mdetdiaglem  19078  mdetrlin  19082  mdetrsca  19083  mdetralt  19088  mdetunilem9  19100  mdetuni0  19101  madutpos  19122  madulid  19125  m2pmfzmap  19226  pmatcollpw3fi1lem1  19265  pm2mp  19304  cpmadugsumlemF  19355  cpmadumatpoly  19362  cayhamlem2  19363  chcoeffeqlem  19364  cayhamlem4  19367  neiptopnei  19611  cnpcl  19727  lmss  19777  pnrmopn  19822  cnt1  19829  1stcelcls  19940  1stccnp  19941  1stckgen  20033  ptbasin  20056  ptpjpre2  20059  ptopn2  20063  dfac14  20097  ptcnplem  20100  ptcnp  20101  txcnmpt  20103  ptcn  20106  prdstps  20108  txcmplem2  20121  hauseqlcld  20125  txlm  20127  lmcn2  20128  qtopeu  20195  ordthmeolem  20280  xkocnv  20293  txflf  20485  ptcmplem3  20532  cnextfres  20546  symgtgp  20578  prdstmdd  20600  prdstgpd  20601  tsmssub  20629  tgptsmscls  20630  tsmssplit  20632  tsmsxplem1  20633  psmetxrge0  20795  imasf1obl  20969  prdsmslem1  21008  prdsxmslem1  21009  prdsxmslem2  21010  metcnp  21022  nmcl  21113  nrginvrcn  21178  nmocl  21205  nmoix  21214  nmoeq0  21221  metdseq0  21336  climcncf  21382  negfcncf  21401  evth  21437  evth2  21438  htpyco1  21456  reparphti  21475  nmhmcn  21581  cphnmcl  21621  lmmbrf  21679  cmetcaulem  21705  iscmet3lem2  21709  lmle  21718  caublcls  21725  bcthlem2  21742  bcthlem3  21743  bcthlem4  21744  rrxnm  21801  rrxcph  21802  rrxds  21803  rrxmval  21810  rrxmetlem  21812  rrxmet  21813  rrxdstprj1  21814  ivth2  21845  evthicc2  21850  cniccbdd  21851  ovolfsf  21861  ovolsf  21862  ovollb2lem  21877  ovolctb  21879  ovolunlem1a  21885  ovolunlem1  21886  ovoliunlem1  21891  ovoliunlem2  21892  ovoliun  21894  ovoliunnul  21896  ovolicc2lem1  21906  ovolicc2lem2  21907  ovolicc2lem4  21909  ovolicc2lem5  21910  voliunlem2  21939  voliunlem3  21940  iunmbl2  21945  ioombl1lem4  21949  ovolfs2  21958  uniiccdif  21965  uniioombllem2a  21969  uniioombllem2  21970  uniioombllem3  21972  uniioombllem6  21975  volivth  21994  vitalilem2  21996  vitalilem4  21998  vitalilem5  21999  mbfmulc2lem  22032  mbfmulc2re  22033  mbfmax  22034  mbfposb  22038  mbfimaopnlem  22040  mbfaddlem  22045  mbfsup  22049  mbflimlem  22052  mbflim  22053  i1fmulclem  22087  itg1mulc  22089  i1fpos  22091  itg1lea  22097  itg1climres  22099  mbfi1fseqlem3  22102  mbfi1fseqlem4  22103  mbfi1fseqlem5  22104  mbfi1fseqlem6  22105  mbfi1flimlem  22107  mbfi1flim  22108  mbfmullem2  22109  itg2uba  22128  itg2mulclem  22131  itg2mulc  22132  itg2monolem1  22135  itg2mono  22138  itg2i1fseqle  22139  itg2i1fseq  22140  itg2i1fseq2  22141  itg2i1fseq3  22142  itg2addlem  22143  itg2gt0  22145  itg2cnlem1  22146  itg2cnlem2  22147  itg2cn  22148  i1fibl  22192  itgitg1  22193  bddmulibl  22223  bddibl  22224  ellimc2  22259  limcres  22268  dvcnp2  22301  dvnf  22308  dvnbss  22309  dvnadd  22310  dvcmulf  22326  dvcof  22329  dvcnv  22356  rolle  22369  cmvth  22370  mvth  22371  dvlip  22372  dvlipcn  22373  dveq0  22379  dv11cn  22380  dvgt0lem1  22381  dvivthlem1  22387  dvivth  22389  dvne0  22390  lhop1lem  22392  lhop1  22393  lhop2  22394  lhop  22395  dvcnvre  22398  ftc1lem1  22414  ftc1lem4  22418  ftc1lem6  22420  ftc2  22423  itgsubst  22428  tdeglem4  22436  mdegleb  22442  mdegnn0cl  22449  mdegaddle  22452  mdegle0  22455  mdegmullem  22456  fta1glem2  22545  elply2  22571  plypf1  22587  plyaddlem1  22588  plymullem1  22589  coeeulem  22599  coeidlem  22612  coeid3  22615  plyco  22616  coemulc  22630  dgrcolem1  22648  dgrcolem2  22649  dgrco  22650  coecj  22653  ofmulrt  22656  dvply2g  22659  plydivlem3  22669  plydiveu  22672  plyrem  22679  vieta1  22686  elqaalem1  22693  elqaalem3  22695  aannenlem1  22702  aannenlem2  22703  taylthlem1  22746  taylthlem2  22747  ulmclm  22760  ulmcaulem  22767  ulmcau  22768  ulmcn  22772  ulmdvlem1  22773  ulmdvlem3  22775  mtest  22777  mtestbdd  22778  mbfulm  22779  iblulm  22780  itgulm  22781  radcnvlem1  22786  radcnvlem2  22787  radcnvlem3  22788  radcnv0  22789  radcnvlt2  22792  dvradcnv  22794  pserulm  22795  psercn2  22796  pserdvlem2  22801  abelthlem1  22804  abelthlem3  22806  abelthlem4  22807  abelthlem5  22808  abelthlem6  22809  abelthlem7  22811  abelthlem8  22812  abelthlem9  22813  abelth  22814  atantayl  23246  leibpi  23251  o1cxp  23282  jensenlem1  23294  jensenlem2  23295  jensen  23296  amgmlem  23297  ftalem4  23327  basellem4  23335  basellem7  23338  basellem9  23340  muinv  23447  dchrmulcl  23502  dchrmulid2  23505  dchrinvcl  23506  dchrinv  23514  dchrptlem2  23518  dchrptlem3  23519  bposlem5  23541  lgsfle1  23558  lgsdchrval  23600  dchrisumlem1  23652  dchrisumlem3  23654  dchrmusum2  23657  dchrisum0re  23676  dchrisum0lem1b  23678  dchrisum0lem2a  23680  f1otrg  24152  fveere  24182  axcontlem5  24249  uhgrass  24284  umgrass  24297  umgran0  24298  umgrale  24299  usgrass  24339  usgraedg2  24353  usgfidegfi  24888  eupap1  24954  numclwlk2lem2f1o  25083  ghgrpOLD  25348  nvcl  25540  nvlmle  25580  blometi  25696  ubthlem1  25764  ubthlem2  25765  minvecolem3  25770  minvecolem4  25774  htthlem  25812  hlimadd  26088  occllem  26199  chscllem1  26533  chscllem2  26534  chscllem4  26536  unopnorm  26814  cnvunop  26815  unopadj  26816  unoplin  26817  hmopre  26820  adjcl  26829  adj2  26831  hmoplin  26839  bracl  26846  lnopmul  26864  homco2  26874  hmopco  26920  adjlnop  26983  adjmul  26989  adjadd  26990  kbass5  27017  leopsq  27026  hmopidmchi  27048  hstcl  27114  foresf1o  27381  iunrdx  27409  disjrdx  27428  ofresid  27460  xppreima2  27466  ofoprabco  27483  isoun  27498  fpwrelmap  27534  rhmdvdsr  27786  tpr2rico  27872  rge0scvg  27909  fsumcvg4  27910  lmxrge0  27912  lmdvg  27913  qqhucn  27951  indsum  28014  indpreima  28016  esumf1o  28039  esumpcvgval  28062  ofcf  28080  ofcfval4  28082  measvxrge0  28154  meascnbl  28168  volmeas  28181  mbfmco2  28214  eulerpartlems  28277  eulerpartlemgc  28279  eulerpartlemd  28283  eulerpartgbij  28289  eulerpartlemgvv  28293  rrvsum  28371  dstfrvunirn  28391  gsumncl  28470  plymul02  28481  signsply0  28486  lgamgulmlem6  28554  lgamgulm2  28556  gamcvg  28576  regamcl  28581  relgamcl  28582  derangenlem  28593  subfacp1lem4  28605  subfacp1lem5  28606  erdszelem9  28621  ptpcon  28656  cvxscon  28666  cvmliftmolem2  28705  cvmliftlem15  28721  cvmlift2lem3  28728  cvmlift3lem4  28745  cvmlift3lem5  28746  cvmlift3lem8  28749  mrsubcv  28848  mrsubff  28850  mrsubrn  28851  mrsubccat  28856  msubff  28868  mvhf  28896  mclsind  28908  mclspps  28922  divcnvlin  29096  iprodefisumlem  29099  faclimlem2  29145  faclim2  29149  ptrest  30024  heicant  30025  mblfinlem2  30028  volsupnfl  30035  itg2addnclem  30042  itg2addnclem2  30043  itg2addnclem3  30044  itg2addnc  30045  itg2gt0cn  30046  bddiblnc  30061  ftc1cnnclem  30064  ftc1cnnc  30065  ftc1anclem3  30068  ftc1anclem4  30069  ftc1anclem5  30070  ftc1anclem6  30071  ftc1anclem7  30072  ftc1anclem8  30073  ftc1anc  30074  ftc2nc  30075  neibastop1  30153  neibastop2lem  30154  filnetlem4  30175  sdclem2  30211  lmclim2  30227  geomcau  30228  ismtybndlem  30278  heiborlem3  30285  heiborlem5  30287  heiborlem6  30288  heiborlem8  30290  heibor  30293  bfplem1  30294  bfplem2  30295  rrnmet  30301  rrndstprj1  30302  rrndstprj2  30303  rrncmslem  30304  ismrer1  30310  ghomdiv  30322  grpokerinj  30323  rngohomcl  30346  ismrcd2  30607  mzpsubst  30657  fphpdo  30727  wepwsolem  30963  hbt  31055  mendlmod  31118  mendassa  31119  radcnvrat  31171  caofcan  31204  ofmul12  31206  fnvinran  31343  rfcnnnub  31365  fmuldfeq  31531  mccllem  31559  clim1fr1  31561  climexp  31565  climinf  31566  climreeq  31573  mullimc  31576  ellimcabssub0  31577  mullimcf  31583  limcrecl  31589  sumnnodd  31590  limsupre  31601  neglimc  31607  addlimc  31608  0ellimcdiv  31609  limclner  31611  sinmulcos  31619  mulcncff  31624  subcncff  31636  addcncff  31641  icccncfext  31644  cncficcgt0  31645  divcncff  31648  cncfiooicclem1  31650  dvsinexp  31659  dvsubf  31663  dvdivf  31673  dvbdfbdioolem2  31680  ioodvbdlimc1lem1  31682  ioodvbdlimc1lem2  31683  ioodvbdlimc2lem  31685  dvnmul  31694  dvnprodlem1  31697  dvnprodlem2  31698  iblcncfioo  31731  itgiccshift  31733  stoweidlem20  31756  wallispilem5  31805  wallispi  31806  stirlinglem8  31817  fourierdlem12  31855  fourierdlem15  31858  fourierdlem22  31865  fourierdlem34  31877  fourierdlem39  31882  fourierdlem41  31884  fourierdlem48  31891  fourierdlem49  31892  fourierdlem50  31893  fourierdlem51  31894  fourierdlem54  31897  fourierdlem56  31899  fourierdlem60  31903  fourierdlem61  31904  fourierdlem62  31905  fourierdlem63  31906  fourierdlem70  31913  fourierdlem72  31915  fourierdlem73  31916  fourierdlem74  31917  fourierdlem75  31918  fourierdlem79  31922  fourierdlem81  31924  fourierdlem82  31925  fourierdlem87  31930  fourierdlem88  31931  fourierdlem92  31935  fourierdlem95  31938  fourierdlem97  31940  fourierdlem101  31944  fourierdlem102  31945  fourierdlem103  31946  fourierdlem104  31947  fourierdlem111  31954  fourierdlem114  31957  fouriersw  31968  etransclem15  31986  etransclem24  31995  etransclem25  31996  etransclem27  31998  etransclem32  32003  etransclem35  32006  etransclem46  32017  uhgss  32323  lincresunit3  32952  lautcl  35686  extoimad  37785  imo72b2lem1  37792  imo72b2  37797
  Copyright terms: Public domain W3C validator