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

Theorem ffvelrnda 5831
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 5829 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 468 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1755   -->wf 5402   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-fv 5414
This theorem is referenced by:  ffvelrnd  5832  f1ocnvdm  5976  foeqcnvco  5985  f1oiso2  6030  suppssof1OLD  6328  ofco  6329  caofref  6335  caofinvl  6336  caofid0l  6337  caofid0r  6338  caofid1  6339  caofid2  6340  caofcom  6341  caofrss  6342  caofass  6343  caoftrn  6344  caofdi  6345  caofdir  6346  caonncan  6347  fnse  6678  suppssof1  6711  suppofss1d  6715  suppofss2d  6716  smofvon  6806  pw2f1olem  7403  mapxpen  7465  xpmapenlem  7466  supisoex  7709  wemappo  7751  wemapsolem  7752  cantnfp1lem1  7874  cantnfp1lem2  7875  cantnfp1lem3  7876  cantnflem1d  7884  cantnflem1  7885  cantnfp1lem1OLD  7900  cantnfp1lem2OLD  7901  cantnfp1lem3OLD  7902  cantnflem1dOLD  7907  cantnflem1OLD  7908  infxpenlem  8168  acndom  8209  acndom2  8212  iunfictbso  8272  ackbij2lem2  8397  cfsmolem  8427  infpssrlem3  8462  infpssrlem4  8463  isf32lem8  8517  isf34lem6  8537  axcc3  8595  axcclem  8614  canthnumlem  8802  ofsubeq0  10306  ofnegsub  10307  ofsubge0  10308  monoord2  11820  seqf1olem2  11829  seqf1o  11830  seqcoll  12199  wrdsymbcl  12229  ccatcl  12257  ccatco  12446  limsupgre  12942  limsupbnd1  12943  limsupbnd2  12944  rlimclim1  13006  rlimuni  13011  rlimresb  13026  o1co  13047  rlimcn1  13049  rlimo1  13077  clim2ser  13115  clim2ser2  13116  isermulc2  13118  iserle  13120  climserle  13123  isercolllem1  13125  isercolllem2  13126  isercoll  13128  caucvgrlem  13133  caucvgr  13136  iseraltlem1  13142  iseraltlem2  13143  iseraltlem3  13144  iseralt  13145  summolem3  13174  summolem2a  13175  fsumf1o  13183  sumss  13184  fsumss  13185  fsumcl2lem  13191  fsumadd  13198  isumclim3  13209  isummulc2  13212  isumrecl  13215  isumadd  13217  fsummulc2  13233  fsumrelem  13252  iserabs  13260  cvgcmp  13261  cvgcmpub  13262  cvgcmpce  13263  isumsplit  13285  climcndslem1  13294  climcndslem2  13295  climcnds  13296  supcvg  13300  mertens  13328  efcj  13359  rpnnen2lem5  13483  rpnnen2lem7  13485  rpnnen2lem8  13486  rpnnen2  13490  ruclem6  13499  ruclem8  13501  ruclem11  13504  ruclem12  13505  nn0seqcvgd  13727  alginv  13732  algcvg  13733  algcvga  13736  algfx  13737  eucalgcvga  13743  eulerthlem1  13838  eulerthlem2  13839  iserodd  13884  pcmptcl  13935  pcmpt  13936  prmreclem6  13964  1arithlem4  13969  vdwlem1  14024  vdwlem2  14025  vdwlem6  14029  vdwlem11  14034  0ram  14063  ramub1lem2  14070  ramcl  14072  imasvscafn  14457  imasvscaf  14459  cofucl  14780  cofulid  14782  funcres2b  14789  funcpropd  14792  ffthiso  14821  fuccocl  14856  fucidcl  14857  fuclid  14858  fucrid  14859  fucass  14860  fucsect  14864  fucinv  14865  invfuc  14866  fuciso  14867  natpropd  14868  fucpropd  14869  setcepi  14938  catcisolem  14956  prfcl  14995  prf1st  14996  prf2nd  14997  1st2ndprf  14998  evlfcl  15014  curfuncf  15030  hofcl  15051  yonedalem4c  15069  yonedainv  15073  yonffthlem  15074  prdsplusgcl  15434  prdsidlem  15435  prdsmndd  15436  pwsco1mhm  15479  pwsco2mhm  15480  gsumval2  15492  gsumwsubmcl  15495  gsumccat  15498  gsumwmhm  15502  grpinvcl  15562  mhmmulg  15638  prdsinvlem  15642  pwsinvg  15646  pwssub  15647  ghminv  15733  symgfv  15871  lactghmga  15888  symgtrinv  15957  psgnunilem5  15979  lsmhash  16181  efginvrel1  16204  efgsrel  16210  frgpuptf  16246  frgpuptinv  16247  frgpup3lem  16253  ghmplusg  16307  prdscmnd  16322  gsumval3eu  16360  gsumval3OLD  16361  gsumval3  16364  gsumzcl2  16368  gsumzf1o  16370  gsumzclOLD  16372  gsumzf1oOLD  16373  gsumzaddlem  16387  gsumzaddlemOLD  16389  gsumzsplit  16397  gsumzsplitOLD  16398  gsumconst  16405  gsumzmhm  16406  gsumzmhmOLD  16407  gsumzoppg  16415  gsumzoppgOLD  16416  gsumsub  16422  gsumsubOLD  16423  gsum2dlem1  16434  gsum2dlem2  16435  gsum2dOLD  16437  dmdprdd  16454  dprdff  16469  dprdfcntz  16472  dprdffOLD  16475  dprdfcntzOLD  16478  dprdfid  16480  dprdfinv  16482  dprdfadd  16483  dprdfsub  16484  dprdf11  16486  dprdfidOLD  16487  dprdfinvOLD  16489  dprdfaddOLD  16490  dprdfsubOLD  16491  dprdf11OLD  16493  dprdsubg  16494  dprdres  16498  dmdprdsplitlem  16507  dmdprdsplitlemOLD  16508  dprdcntz2  16509  dprd2da  16514  dmdprdsplit2lem  16517  ablfac1c  16545  ablfac1eu  16547  ablfaclem2  16560  ablfaclem3  16561  ablfac2  16563  prdsmulrcl  16637  prdsrngd  16638  isabvd  16828  abvcl  16832  abvge0  16833  srngcl  16863  lcomfsupOLD  16907  lcomfsupp  16908  prdsvscacl  16970  prdslmodd  16971  lmhmco  17045  lmhmvsca  17047  lmhmf1o  17048  pwssplit2  17062  pwssplit3  17063  rrgsupp  17283  rrgsuppOLD  17284  psrbagcon  17373  psrbaglefi  17374  psrbaglefiOLD  17375  psrbagconf1o  17377  gsumbagdiaglem  17378  psrass1lem  17380  psrlinv  17401  psrlidm  17407  psrlidmOLD  17408  psrridm  17409  psrridmOLD  17410  psrass1  17411  psrcom  17414  mplsubrglem  17450  mplsubrglemOLD  17451  mplmonmul  17476  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  mplbas2  17482  mplbas2OLD  17483  mplcoe4  17516  evlslem2  17524  psrplusgpropd  17587  coe1subfv  17617  ply1coe  17642  gsumfsum  17722  zntoslem  17830  cygznlem3  17843  frgpcyg  17847  psgninv  17853  dsmmacl  18007  dsmmsubg  18009  dsmmlss  18010  frlmphl  18047  uvcresum  18059  frlmsslsp  18064  frlmsslspOLD  18065  frlmup1  18067  grpvrinv  18137  mhmvlin  18138  mdetleib2  18240  mdetf  18247  mdetcl  18248  mdet1  18249  mdetrlin  18250  mdetrsca  18251  mdetralt  18255  mdetunilem9  18267  mdetuni0  18268  madutpos  18289  madulid  18292  matunit  18325  neiptopnei  18577  cnpcl  18693  lmss  18743  pnrmopn  18788  cnt1  18795  1stcelcls  18906  1stccnp  18907  1stckgen  18968  ptbasin  18991  ptpjpre2  18994  ptopn2  18998  dfac14  19032  ptcnplem  19035  ptcnp  19036  txcnmpt  19038  ptcn  19041  prdstps  19043  txcmplem2  19056  hauseqlcld  19060  txlm  19062  lmcn2  19063  qtopeu  19130  ordthmeolem  19215  xkocnv  19228  txflf  19420  ptcmplem3  19467  cnextfres  19481  symgtgp  19513  prdstmdd  19535  prdstgpd  19536  tsmssub  19564  tgptsmscls  19565  tsmssplit  19567  tsmsxplem1  19568  psmetxrge0  19730  imasf1obl  19904  prdsmslem1  19943  prdsxmslem1  19944  prdsxmslem2  19945  metcnp  19957  nmcl  20048  nrginvrcn  20113  nmocl  20140  nmoix  20149  nmoeq0  20156  metdseq0  20271  climcncf  20317  negfcncf  20336  evth  20372  evth2  20373  htpyco1  20391  reparphti  20410  nmhmcn  20516  cphnmcl  20556  lmmbrf  20614  cmetcaulem  20640  iscmet3lem2  20644  lmle  20653  caublcls  20660  bcthlem2  20677  bcthlem3  20678  bcthlem4  20679  rrxnm  20736  rrxcph  20737  rrxds  20738  rrxmval  20745  rrxmetlem  20747  rrxmet  20748  rrxdstprj1  20749  ivth2  20780  evthicc2  20785  cniccbdd  20786  ovolfsf  20796  ovolsf  20797  ovollb2lem  20812  ovolctb  20814  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliunlem2  20827  ovoliun  20829  ovoliunnul  20831  ovolicc2lem1  20841  ovolicc2lem2  20842  ovolicc2lem4  20844  ovolicc2lem5  20845  voliunlem2  20873  voliunlem3  20874  iunmbl2  20879  ioombl1lem4  20883  ovolfs2  20892  uniiccdif  20899  uniioombllem2a  20903  uniioombllem2  20904  uniioombllem3  20906  uniioombllem6  20909  volivth  20928  vitalilem2  20930  vitalilem4  20932  vitalilem5  20933  mbfmulc2lem  20966  mbfmulc2re  20967  mbfmax  20968  mbfposb  20972  mbfimaopnlem  20974  mbfaddlem  20979  mbfsup  20983  mbflimlem  20986  mbflim  20987  i1fmulclem  21021  itg1mulc  21023  i1fpos  21025  itg1lea  21031  itg1climres  21033  mbfi1fseqlem3  21036  mbfi1fseqlem4  21037  mbfi1fseqlem5  21038  mbfi1fseqlem6  21039  mbfi1flimlem  21041  mbfi1flim  21042  mbfmullem2  21043  itg2uba  21062  itg2mulclem  21065  itg2mulc  21066  itg2monolem1  21069  itg2mono  21072  itg2i1fseqle  21073  itg2i1fseq  21074  itg2i1fseq2  21075  itg2i1fseq3  21076  itg2addlem  21077  itg2gt0  21079  itg2cnlem1  21080  itg2cnlem2  21081  itg2cn  21082  i1fibl  21126  itgitg1  21127  bddmulibl  21157  bddibl  21158  ellimc2  21193  limcres  21202  dvcnp2  21235  dvnf  21242  dvnbss  21243  dvnadd  21244  dvcmulf  21260  dvcof  21263  dvcnv  21290  rolle  21303  cmvth  21304  mvth  21305  dvlip  21306  dvlipcn  21307  dveq0  21313  dv11cn  21314  dvgt0lem1  21315  dvivthlem1  21321  dvivth  21323  dvne0  21324  lhop1lem  21326  lhop1  21327  lhop2  21328  lhop  21329  dvcnvre  21332  ftc1lem1  21348  ftc1lem4  21352  ftc1lem6  21354  ftc2  21357  itgsubst  21362  evlslem6  21363  evlslem6OLD  21364  evlslem1  21366  pf1mpf  21402  pf1ind  21405  tdeglem4  21413  mdegleb  21419  mdegnn0cl  21426  mdegaddle  21429  mdegle0  21432  mdegmullem  21433  deg1sclle  21468  deg1scl  21469  fta1glem2  21522  elply2  21548  plypf1  21564  plyaddlem1  21565  plymullem1  21566  coeeulem  21576  coeidlem  21589  coeid3  21592  plyco  21593  coemulc  21606  dgrcolem1  21624  dgrcolem2  21625  dgrco  21626  coecj  21629  ofmulrt  21632  dvply2g  21635  plydivlem3  21645  plydiveu  21648  plyrem  21655  vieta1  21662  elqaalem1  21669  elqaalem3  21671  aannenlem1  21678  aannenlem2  21679  taylthlem1  21722  taylthlem2  21723  ulmclm  21736  ulmcaulem  21743  ulmcau  21744  ulmcn  21748  ulmdvlem1  21749  ulmdvlem3  21751  mtest  21753  mtestbdd  21754  mbfulm  21755  iblulm  21756  itgulm  21757  radcnvlem1  21762  radcnvlem2  21763  radcnvlem3  21764  radcnv0  21765  radcnvlt2  21768  dvradcnv  21770  pserulm  21771  psercn2  21772  pserdvlem2  21777  abelthlem1  21780  abelthlem3  21782  abelthlem4  21783  abelthlem5  21784  abelthlem6  21785  abelthlem7  21787  abelthlem8  21788  abelthlem9  21789  abelth  21790  atantayl  22216  leibpi  22221  o1cxp  22252  jensenlem1  22264  jensenlem2  22265  jensen  22266  amgmlem  22267  ftalem4  22297  basellem4  22305  basellem7  22308  basellem9  22310  muinv  22417  dchrmulcl  22472  dchrmulid2  22475  dchrinvcl  22476  dchrinv  22484  dchrptlem2  22488  dchrptlem3  22489  bposlem5  22511  lgsfle1  22528  lgsdchrval  22570  dchrisumlem1  22622  dchrisumlem3  22624  dchrmusum2  22627  dchrisum0re  22646  dchrisum0lem1b  22648  dchrisum0lem2a  22650  f1otrg  22939  fveere  22969  axcontlem5  23036  uhgrass  23062  umgrass  23075  umgran0  23076  umgrale  23077  usgrass  23105  usgraedg2  23116  eupap1  23419  ghgrp  23677  nvcl  23869  nvlmle  23909  blometi  24025  ubthlem1  24093  ubthlem2  24094  minvecolem3  24099  minvecolem4  24103  htthlem  24141  hlimadd  24417  occllem  24528  chscllem1  24862  chscllem2  24863  chscllem4  24865  unopnorm  25143  cnvunop  25144  unopadj  25145  unoplin  25146  hmopre  25149  adjcl  25158  adj2  25160  hmoplin  25168  bracl  25175  lnopmul  25193  homco2  25203  hmopco  25249  adjlnop  25312  adjmul  25318  adjadd  25319  kbass5  25346  leopsq  25355  hmopidmchi  25377  hstcl  25443  iunrdx  25737  disjrdx  25756  ofresid  25783  xppreima2  25788  ofoprabco  25805  isoun  25820  fpwrelmap  25857  rhmdvdsr  26138  tpr2rico  26195  rge0scvg  26232  fsumcvg4  26233  lmxrge0  26235  lmdvg  26236  qqhucn  26274  indsum  26332  indpreima  26334  esumf1o  26357  esumpcvgval  26380  ofcf  26398  ofcfval4  26400  measvxrge0  26472  meascnbl  26486  volmeas  26500  mbfmco2  26533  eulerpartlems  26590  eulerpartlemgc  26592  eulerpartlemd  26596  eulerpartgbij  26602  eulerpartlemgvv  26606  rrvsum  26684  dstfrvunirn  26704  gsumncl  26783  plymul02  26794  signsply0  26799  lgamgulmlem6  26867  lgamgulm2  26869  gamcvg  26889  regamcl  26894  relgamcl  26895  derangenlem  26906  subfacp1lem4  26918  subfacp1lem5  26919  erdszelem9  26934  ptpcon  26969  cvxscon  26979  cvmliftmolem2  27018  cvmliftlem15  27034  cvmlift2lem3  27041  cvmlift3lem4  27058  cvmlift3lem5  27059  cvmlift3lem8  27062  divcnvlin  27245  clim2prod  27249  clim2div  27250  prodfdiv  27257  ntrivcvgtail  27261  ntrivcvgmullem  27262  prodmolem3  27292  prodmolem2a  27293  fprodf1o  27305  prodss  27306  fprodss  27307  fprodser  27308  fprodcl2lem  27309  fprodmul  27317  fproddiv  27318  fprodefsum  27331  fprodn0  27336  iprodclim3  27346  iprodrecl  27348  iprodmul  27349  iprodefisumlem  27350  faclimlem2  27396  faclim2  27400  ptrest  28266  heicant  28267  mblfinlem2  28270  volsupnfl  28277  itg2addnclem  28284  itg2addnclem2  28285  itg2addnclem3  28286  itg2addnc  28287  itg2gt0cn  28288  bddiblnc  28303  ftc1cnnclem  28306  ftc1cnnc  28307  ftc1anclem3  28310  ftc1anclem4  28311  ftc1anclem5  28312  ftc1anclem6  28313  ftc1anclem7  28314  ftc1anclem8  28315  ftc1anc  28316  ftc2nc  28317  neibastop1  28421  neibastop2lem  28422  filnetlem4  28443  sdclem2  28479  lmclim2  28495  geomcau  28496  ismtybndlem  28546  heiborlem3  28553  heiborlem5  28555  heiborlem6  28556  heiborlem8  28558  heibor  28561  bfplem1  28562  bfplem2  28563  rrnmet  28569  rrndstprj1  28570  rrndstprj2  28571  rrncmslem  28572  ismrer1  28578  ghomdiv  28590  grpokerinj  28591  rngohomcl  28614  ismrcd2  28877  mzpsubst  28927  fphpdo  28998  wepwsolem  29236  hbt  29328  mendlmod  29392  mendassa  29393  caofcan  29439  ofmul12  29441  fnvinran  29578  rfcnnnub  29600  fmuldfeq  29606  clim1fr1  29617  climexp  29621  climinf  29622  climreeq  29629  dvsinexp  29630  stoweidlem20  29658  wallispilem5  29707  wallispi  29708  stirlinglem8  29719  usgfidegfi  30370  numclwlk2lem2f1o  30541  lincresunit3  30721  lautcl  33301
  Copyright terms: Public domain W3C validator