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

Theorem ffvelrnda 6007
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 6005 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
31, 2sylan 469 1  |-  ( (
ph  /\  C  e.  A )  ->  ( F `  C )  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   -->wf 5566   ` cfv 5570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-fv 5578
This theorem is referenced by:  ffvelrnd  6008  f1ocnvdm  6163  foeqcnvco  6178  f1oiso2  6223  suppssof1OLD  6532  ofco  6533  caofref  6539  caofinvl  6540  caofid0l  6541  caofid0r  6542  caofid1  6543  caofid2  6544  caofcom  6545  caofrss  6546  caofass  6547  caoftrn  6548  caofdi  6549  caofdir  6550  caonncan  6551  fnse  6890  suppssof1  6925  suppofss1d  6929  suppofss2d  6930  smofvon  7022  pw2f1olem  7614  mapxpen  7676  xpmapenlem  7677  supisoex  7924  wemappo  7966  wemapsolem  7967  cantnfp1lem1  8088  cantnfp1lem2  8089  cantnfp1lem3  8090  cantnflem1d  8098  cantnflem1  8099  cantnfp1lem1OLD  8114  cantnfp1lem2OLD  8115  cantnfp1lem3OLD  8116  cantnflem1dOLD  8121  cantnflem1OLD  8122  infxpenlem  8382  acndom  8423  acndom2  8426  iunfictbso  8486  ackbij2lem2  8611  cfsmolem  8641  infpssrlem3  8676  infpssrlem4  8677  isf32lem8  8731  isf34lem6  8751  axcc3  8809  axcclem  8828  canthnumlem  9015  ofsubeq0  10528  ofnegsub  10529  ofsubge0  10530  monoord2  12123  seqf1olem2  12132  seqf1o  12133  seqcoll  12499  wrdsymbcl  12549  ccatcl  12585  ccatco  12795  limsupgre  13389  limsupbnd1  13390  limsupbnd2  13391  rlimclim1  13453  rlimuni  13458  rlimresb  13473  o1co  13494  rlimcn1  13496  rlimo1  13524  clim2ser  13562  clim2ser2  13563  isermulc2  13565  iserle  13567  climserle  13570  isercolllem1  13572  isercolllem2  13573  isercoll  13575  caucvgrlem  13580  caucvgr  13583  iseraltlem1  13589  iseraltlem2  13590  iseraltlem3  13591  iseralt  13592  summolem3  13621  summolem2a  13622  fsumf1o  13630  sumss  13631  fsumss  13632  fsumcl2lem  13638  fsumadd  13646  isumclim3  13659  isummulc2  13662  isumrecl  13665  isumadd  13667  fsummulc2  13684  fsumrelem  13706  iserabs  13714  cvgcmp  13715  cvgcmpub  13716  cvgcmpce  13717  isumsplit  13737  climcndslem1  13746  climcndslem2  13747  climcnds  13748  supcvg  13752  mertens  13780  clim2prod  13782  clim2div  13783  prodfdiv  13790  ntrivcvgtail  13794  ntrivcvgmullem  13795  prodmolem3  13825  prodmolem2a  13826  fprodf1o  13838  prodss  13839  fprodss  13840  fprodser  13841  fprodcl2lem  13842  fprodmul  13850  fproddiv  13851  fprodn0  13868  iprodclim3  13878  iprodrecl  13880  iprodmul  13881  efcj  13912  fprodefsum  13915  rpnnen2lem5  14039  rpnnen2lem7  14041  rpnnen2lem8  14042  rpnnen2  14046  ruclem6  14055  ruclem8  14057  ruclem11  14060  ruclem12  14061  nn0seqcvgd  14286  alginv  14291  algcvg  14292  algcvga  14295  algfx  14296  eucalgcvga  14302  eulerthlem1  14398  eulerthlem2  14399  iserodd  14446  pcmptcl  14497  pcmpt  14498  prmreclem6  14526  1arithlem4  14531  vdwlem1  14586  vdwlem2  14587  vdwlem6  14591  vdwlem11  14596  0ram  14625  ramub1lem2  14632  ramcl  14634  imasvscafn  15029  imasvscaf  15031  cofucl  15379  cofulid  15381  funcres2b  15388  funcpropd  15391  ffthiso  15420  fuccocl  15455  fucidcl  15456  fuclid  15457  fucrid  15458  fucass  15459  fucsect  15463  fucinv  15464  invfuc  15465  fuciso  15466  natpropd  15467  fucpropd  15468  setcepi  15569  catcisolem  15587  prfcl  15674  prf1st  15675  prf2nd  15676  1st2ndprf  15677  evlfcl  15693  curfuncf  15709  hofcl  15730  yonedalem4c  15748  yonedainv  15752  yonffthlem  15753  gsumval2  16109  prdsplusgcl  16153  prdsidlem  16154  prdsmndd  16155  pwsco1mhm  16203  pwsco2mhm  16204  gsumwsubmcl  16208  gsumccat  16211  gsumwmhm  16215  grpinvcl  16297  mhmmulg  16376  prdsinvlem  16380  pwsinvg  16384  pwssub  16385  ghminv  16476  symgfv  16614  lactghmga  16631  symgtrinv  16699  psgnunilem5  16721  lsmhash  16925  efginvrel1  16948  efgsrel  16954  frgpuptf  16990  frgpuptinv  16991  frgpup3lem  16997  ghmplusg  17054  prdscmnd  17069  gsumval3eu  17109  gsumval3OLD  17110  gsumval3  17113  gsumzcl2  17117  gsumzf1o  17119  gsumzclOLD  17121  gsumzf1oOLD  17122  gsumzaddlem  17136  gsumzaddlemOLD  17138  gsumzsplit  17146  gsumzsplitOLD  17147  gsumconst  17155  gsumzmhm  17158  gsumzmhmOLD  17159  gsumzoppg  17168  gsumzoppgOLD  17169  gsumsub  17174  gsum2dlem1  17196  gsum2dlem2  17197  gsum2dOLD  17199  dmdprdd  17228  dprdff  17244  dprdfcntz  17247  dprdffOLD  17250  dprdfcntzOLD  17253  dprdfid  17255  dprdfinv  17257  dprdfadd  17258  dprdfsub  17259  dprdf11  17261  dprdfidOLD  17262  dprdfinvOLD  17264  dprdfaddOLD  17265  dprdfsubOLD  17266  dprdf11OLD  17268  dprdsubg  17269  dprdres  17273  dprdf1o  17277  dmdprdsplitlem  17282  dmdprdsplitlemOLD  17283  dprdcntz2  17284  dprd2da  17289  dmdprdsplit2lem  17292  ablfac1c  17320  ablfac1eu  17322  ablfaclem2  17335  ablfaclem3  17336  ablfac2  17338  prdsmulrcl  17458  prdsringd  17459  isabvd  17667  abvcl  17671  abvge0  17672  srngcl  17702  lcomfsupOLD  17747  lcomfsupp  17748  prdsvscacl  17812  prdslmodd  17813  lmhmco  17887  lmhmvsca  17889  lmhmf1o  17890  pwssplit2  17904  pwssplit3  17905  rrgsupp  18137  rrgsuppOLD  18138  psrbagcon  18220  psrbaglefi  18221  psrbaglefiOLD  18222  psrbagconf1o  18224  gsumbagdiaglem  18225  psrass1lem  18227  psrlinv  18248  psrlidm  18254  psrlidmOLD  18255  psrridm  18256  psrridmOLD  18257  psrass1  18258  psrcom  18262  mplsubrglem  18298  mplsubrglemOLD  18299  mplmonmul  18324  mplcoe1  18325  mplcoe5lem  18328  mplcoe5  18329  mplcoe2OLD  18331  mplbas2  18332  mplbas2OLD  18333  mplcoe4  18366  evlslem2  18378  evlslem6  18379  evlslem6OLD  18380  evlslem1  18382  coe1fvalcl  18449  psrplusgpropd  18475  coe1subfv  18505  ply1sclcl  18525  ply1coe  18535  ply1coeOLD  18536  pf1mpf  18586  pf1ind  18589  gsumfsum  18682  zntoslem  18771  cygznlem3  18784  frgpcyg  18788  psgninv  18794  dsmmacl  18948  dsmmsubg  18950  dsmmlss  18951  frlmphl  18986  uvcresum  18998  frlmsslsp  19001  frlmup1  19003  grpvrinv  19068  mhmvlin  19069  mdetleib2  19260  mdetf  19267  mdetcl  19268  mdetdiaglem  19270  mdetrlin  19274  mdetrsca  19275  mdetralt  19280  mdetunilem9  19292  mdetuni0  19293  madutpos  19314  madulid  19317  m2pmfzmap  19418  pmatcollpw3fi1lem1  19457  pm2mp  19496  cpmadugsumlemF  19547  cpmadumatpoly  19554  cayhamlem2  19555  chcoeffeqlem  19556  cayhamlem4  19559  neiptopnei  19803  cnpcl  19919  lmss  19969  pnrmopn  20014  cnt1  20021  1stcelcls  20131  1stccnp  20132  1stckgen  20224  ptbasin  20247  ptpjpre2  20250  ptopn2  20254  dfac14  20288  ptcnplem  20291  ptcnp  20292  txcnmpt  20294  ptcn  20297  prdstps  20299  txcmplem2  20312  hauseqlcld  20316  txlm  20318  lmcn2  20319  qtopeu  20386  ordthmeolem  20471  xkocnv  20484  txflf  20676  ptcmplem3  20723  cnextfres  20737  symgtgp  20769  prdstmdd  20791  prdstgpd  20792  tsmssub  20820  tgptsmscls  20821  tsmssplit  20823  tsmsxplem1  20824  psmetxrge0  20986  imasf1obl  21160  prdsmslem1  21199  prdsxmslem1  21200  prdsxmslem2  21201  metcnp  21213  nmcl  21304  nrginvrcn  21369  nmocl  21396  nmoix  21405  nmoeq0  21412  metdseq0  21527  climcncf  21573  negfcncf  21592  evth  21628  evth2  21629  htpyco1  21647  reparphti  21666  nmhmcn  21772  cphnmcl  21812  lmmbrf  21870  cmetcaulem  21896  iscmet3lem2  21900  lmle  21909  caublcls  21916  bcthlem2  21933  bcthlem3  21934  bcthlem4  21935  rrxnm  21992  rrxcph  21993  rrxds  21994  rrxmval  22001  rrxmetlem  22003  rrxmet  22004  rrxdstprj1  22005  ivth2  22036  evthicc2  22041  cniccbdd  22042  ovolfsf  22052  ovolsf  22053  ovollb2lem  22068  ovolctb  22070  ovolunlem1a  22076  ovolunlem1  22077  ovoliunlem1  22082  ovoliunlem2  22083  ovoliun  22085  ovoliunnul  22087  ovolicc2lem1  22097  ovolicc2lem2  22098  ovolicc2lem4  22100  ovolicc2lem5  22101  voliunlem2  22130  voliunlem3  22131  iunmbl2  22136  ioombl1lem4  22140  ovolfs2  22149  uniiccdif  22156  uniioombllem2a  22160  uniioombllem2  22161  uniioombllem3  22163  uniioombllem6  22166  volivth  22185  vitalilem2  22187  vitalilem4  22189  vitalilem5  22190  mbfmulc2lem  22223  mbfmulc2re  22224  mbfmax  22225  mbfposb  22229  mbfimaopnlem  22231  mbfaddlem  22236  mbfsup  22240  mbflimlem  22243  mbflim  22244  i1fmulclem  22278  itg1mulc  22280  i1fpos  22282  itg1lea  22288  itg1climres  22290  mbfi1fseqlem3  22293  mbfi1fseqlem4  22294  mbfi1fseqlem5  22295  mbfi1fseqlem6  22296  mbfi1flimlem  22298  mbfi1flim  22299  mbfmullem2  22300  itg2uba  22319  itg2mulclem  22322  itg2mulc  22323  itg2monolem1  22326  itg2mono  22329  itg2i1fseqle  22330  itg2i1fseq  22331  itg2i1fseq2  22332  itg2i1fseq3  22333  itg2addlem  22334  itg2gt0  22336  itg2cnlem1  22337  itg2cnlem2  22338  itg2cn  22339  i1fibl  22383  itgitg1  22384  bddmulibl  22414  bddibl  22415  ellimc2  22450  limcres  22459  dvcnp2  22492  dvnf  22499  dvnbss  22500  dvnadd  22501  dvcmulf  22517  dvcof  22520  dvcnv  22547  rolle  22560  cmvth  22561  mvth  22562  dvlip  22563  dvlipcn  22564  dveq0  22570  dv11cn  22571  dvgt0lem1  22572  dvivthlem1  22578  dvivth  22580  dvne0  22581  lhop1lem  22583  lhop1  22584  lhop2  22585  lhop  22586  dvcnvre  22589  ftc1lem1  22605  ftc1lem4  22609  ftc1lem6  22611  ftc2  22614  itgsubst  22619  tdeglem4  22627  mdegleb  22633  mdegnn0cl  22640  mdegaddle  22643  mdegle0  22646  mdegmullem  22647  fta1glem2  22736  elply2  22762  plypf1  22778  plyaddlem1  22779  plymullem1  22780  coeeulem  22790  coeidlem  22803  coeid3  22806  plyco  22807  coemulc  22821  dgrcolem1  22839  dgrcolem2  22840  dgrco  22841  coecj  22844  ofmulrt  22847  dvply2g  22850  plydivlem3  22860  plydiveu  22863  plyrem  22870  vieta1  22877  elqaalem1  22884  elqaalem3  22886  aannenlem1  22893  aannenlem2  22894  taylthlem1  22937  taylthlem2  22938  ulmclm  22951  ulmcaulem  22958  ulmcau  22959  ulmcn  22963  ulmdvlem1  22964  ulmdvlem3  22966  mtest  22968  mtestbdd  22969  mbfulm  22970  iblulm  22971  itgulm  22972  radcnvlem1  22977  radcnvlem2  22978  radcnvlem3  22979  radcnv0  22980  radcnvlt2  22983  dvradcnv  22985  pserulm  22986  psercn2  22987  pserdvlem2  22992  abelthlem1  22995  abelthlem3  22997  abelthlem4  22998  abelthlem5  22999  abelthlem6  23000  abelthlem7  23002  abelthlem8  23003  abelthlem9  23004  abelth  23005  atantayl  23468  leibpi  23473  o1cxp  23505  jensenlem1  23517  jensenlem2  23518  jensen  23519  amgmlem  23520  ftalem4  23550  basellem4  23558  basellem7  23561  basellem9  23563  muinv  23670  dchrmulcl  23725  dchrmulid2  23728  dchrinvcl  23729  dchrinv  23737  dchrptlem2  23741  dchrptlem3  23742  bposlem5  23764  lgsfle1  23781  lgsdchrval  23823  dchrisumlem1  23875  dchrisumlem3  23877  dchrmusum2  23880  dchrisum0re  23899  dchrisum0lem1b  23901  dchrisum0lem2a  23903  f1otrg  24379  fveere  24409  axcontlem5  24476  uhgrass  24511  umgrass  24524  umgran0  24525  umgrale  24526  usgrass  24566  usgraedg2  24580  usgfidegfi  25115  eupap1  25181  numclwlk2lem2f1o  25310  ghgrpOLD  25571  nvcl  25763  nvlmle  25803  blometi  25919  ubthlem1  25987  ubthlem2  25988  minvecolem3  25993  minvecolem4  25997  htthlem  26035  hlimadd  26311  occllem  26422  chscllem1  26756  chscllem2  26757  chscllem4  26759  unopnorm  27037  cnvunop  27038  unopadj  27039  unoplin  27040  hmopre  27043  adjcl  27052  adj2  27054  hmoplin  27062  bracl  27069  lnopmul  27087  homco2  27097  hmopco  27143  adjlnop  27206  adjmul  27212  adjadd  27213  kbass5  27240  leopsq  27249  hmopidmchi  27271  hstcl  27337  foresf1o  27605  iunrdx  27644  disjrdx  27664  ofresid  27706  xppreima2  27712  ofoprabco  27735  isoun  27751  fpwrelmap  27790  rhmdvdsr  28046  tpr2rico  28132  rge0scvg  28169  fsumcvg4  28170  lmxrge0  28172  lmdvg  28173  qqhucn  28210  indsum  28255  indpreima  28257  esumf1o  28282  esumpcvgval  28310  ofcf  28335  ofcfval4  28337  measvxrge0  28416  meascnbl  28430  volmeas  28443  mbfmco2  28476  omssubadd  28511  0elcarsg  28518  inelcarsg  28522  carsgclctun  28532  eulerpartlems  28566  eulerpartlemgc  28568  eulerpartlemd  28572  eulerpartgbij  28578  eulerpartlemgvv  28582  rrvsum  28660  dstfrvunirn  28680  gsumncl  28759  plymul02  28770  signsply0  28775  lgamgulmlem6  28843  lgamgulm2  28845  gamcvg  28865  regamcl  28870  relgamcl  28871  derangenlem  28882  subfacp1lem4  28894  subfacp1lem5  28895  erdszelem9  28910  ptpcon  28945  cvxscon  28955  cvmliftmolem2  28994  cvmliftlem15  29010  cvmlift2lem3  29017  cvmlift3lem4  29034  cvmlift3lem5  29035  cvmlift3lem8  29038  mrsubcv  29137  mrsubff  29139  mrsubrn  29140  mrsubccat  29145  msubff  29157  mvhf  29185  mclsind  29197  mclspps  29211  divcnvlin  29362  iprodefisumlem  29367  faclimlem2  29413  faclim2  29417  ptrest  30291  heicant  30292  mblfinlem2  30295  volsupnfl  30302  itg2addnclem  30309  itg2addnclem2  30310  itg2addnclem3  30311  itg2addnc  30312  itg2gt0cn  30313  bddiblnc  30328  ftc1cnnclem  30331  ftc1cnnc  30332  ftc1anclem3  30335  ftc1anclem4  30336  ftc1anclem5  30337  ftc1anclem6  30338  ftc1anclem7  30339  ftc1anclem8  30340  ftc1anc  30341  ftc2nc  30342  neibastop1  30420  neibastop2lem  30421  filnetlem4  30442  sdclem2  30478  lmclim2  30494  geomcau  30495  ismtybndlem  30545  heiborlem3  30552  heiborlem5  30554  heiborlem6  30555  heiborlem8  30557  heibor  30560  bfplem1  30561  bfplem2  30562  rrnmet  30568  rrndstprj1  30569  rrndstprj2  30570  rrncmslem  30571  ismrer1  30577  ghomdiv  30589  grpokerinj  30590  rngohomcl  30613  ismrcd2  30874  mzpsubst  30923  fphpdo  30993  wepwsolem  31229  hbt  31323  mendlmod  31386  mendassa  31387  radcnvrat  31439  caofcan  31472  ofmul12  31474  binomcxplemnn0  31498  fnvinran  31632  rfcnnnub  31654  fmuldfeq  31819  mccllem  31847  clim1fr1  31849  climexp  31853  climinf  31854  climreeq  31861  mullimc  31864  ellimcabssub0  31865  mullimcf  31871  limcrecl  31877  sumnnodd  31878  limsupre  31889  neglimc  31895  addlimc  31896  0ellimcdiv  31897  limclner  31899  sinmulcos  31907  mulcncff  31912  subcncff  31924  addcncff  31929  icccncfext  31932  cncficcgt0  31933  divcncff  31936  cncfiooicclem1  31938  dvsinexp  31947  dvsubf  31951  dvdivf  31961  dvbdfbdioolem2  31968  ioodvbdlimc1lem1  31970  ioodvbdlimc1lem2  31971  ioodvbdlimc2lem  31973  dvnmul  31982  dvnprodlem1  31985  dvnprodlem2  31986  iblcncfioo  32019  itgiccshift  32021  stoweidlem20  32044  wallispilem5  32093  wallispi  32094  stirlinglem8  32105  fourierdlem12  32143  fourierdlem15  32146  fourierdlem22  32153  fourierdlem34  32165  fourierdlem39  32170  fourierdlem41  32172  fourierdlem48  32179  fourierdlem49  32180  fourierdlem50  32181  fourierdlem51  32182  fourierdlem54  32185  fourierdlem56  32187  fourierdlem60  32191  fourierdlem61  32192  fourierdlem62  32193  fourierdlem63  32194  fourierdlem70  32201  fourierdlem72  32203  fourierdlem73  32204  fourierdlem74  32205  fourierdlem75  32206  fourierdlem79  32210  fourierdlem81  32212  fourierdlem82  32213  fourierdlem87  32218  fourierdlem88  32219  fourierdlem92  32223  fourierdlem95  32226  fourierdlem97  32228  fourierdlem101  32232  fourierdlem102  32233  fourierdlem103  32234  fourierdlem104  32235  fourierdlem111  32242  fourierdlem114  32245  fouriersw  32256  etransclem15  32274  etransclem24  32283  etransclem25  32284  etransclem27  32286  etransclem32  32291  etransclem35  32294  etransclem46  32305  uhgss  32760  lincresunit3  33355  elbigolo1  33451  lautcl  36227  extoimad  38494  imo72b2lem1  38501  imo72b2  38506
  Copyright terms: Public domain W3C validator