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

Theorem ffvelrn 6035
Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)
Assertion
Ref Expression
ffvelrn  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )

Proof of Theorem ffvelrn
StepHypRef Expression
1 ffn 5739 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 6034 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 479 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5747 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3417 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 472 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
73, 6mpd 15 1  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376    e. wcel 1904   ran crn 4840    Fn wfn 5584   -->wf 5585   ` cfv 5589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-sbc 3256  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-id 4754  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-fv 5597
This theorem is referenced by:  ffvelrni  6036  ffvelrnda  6037  dffo3  6052  foco2  6057  ffnfv  6064  ffvresb  6070  fcompt  6075  fsn2  6078  fvconst  6098  fcofo  6204  cocan1  6207  isocnv  6239  isocnv3  6241  isores2  6242  isopolem  6254  isosolem  6256  fovrn  6458  off  6565  fnwelem  6930  smofvon2  7093  smorndom  7105  omsmolem  7372  omsmo  7373  mapsncnv  7536  2dom  7660  xpdom2  7685  domunsncan  7690  xpmapenlem  7757  fiint  7866  ordiso2  8048  infdifsn  8180  cantnflem1  8212  wemapwe  8220  cnfcom3lem  8226  fseqenlem1  8473  finacn  8499  ackbij1lem12  8679  cofsmo  8717  cfsmolem  8718  cfcoflem  8720  coftr  8721  isf32lem6  8806  isf32lem7  8807  isf34lem7  8827  isf34lem6  8828  acncc  8888  axdc2lem  8896  axdc3lem2  8899  axdc3lem4  8901  axdc4lem  8903  axcclem  8905  ttukeylem6  8962  alephreg  9025  pwcfsdom  9026  canthp1lem2  9096  canthp1  9097  pwfseqlem1  9101  pwfseqlem4a  9104  gruf  9254  fsequb2  12227  axdc4uzlem  12233  seqf1o  12292  hashf1lem1  12659  wwlktovf  13106  shftf  13219  limsupgre  13619  limsupgreOLD  13620  rlimuni  13691  lo1resb  13705  o1resb  13707  o1of2  13753  o1rlimmul  13759  isercolllem1  13805  isercolllem2  13806  isercolllem3  13807  isercoll  13808  climsup  13810  iseralt  13828  sumeq2ii  13836  summolem2a  13858  isumcl  13899  isumshft  13974  climcndslem2  13985  climcnds  13986  mertenslem2  14018  prodeq2ii  14044  prodmolem2a  14065  iprodcl  14131  rpnnen2lem10  14353  ruclem8  14366  ruclem12  14370  3dvds  14448  smueqlem  14543  nn0seqcvgd  14608  algrf  14611  eucalg  14625  phimullem  14806  pcmpt  14916  pcprod  14919  vdwlem11  15020  vdwnnlem3  15026  ramlb  15056  0ram  15057  ramcl  15066  prmgaplcmlem1OLD  15091  prmgaplcmlem2OLD  15092  prmdvdsprmorpOLD  15095  prmgapprmorlemOLD  15096  prmorlelcmfOLD  15099  prmorlelcmsOLDOLD  15101  prmgaplem8  15107  imasaddfnlem  15512  imasaddflem  15514  mhmpropd  16666  ghmsub  16969  cntzmhm  17070  f1omvdconj  17165  pj1ghm  17431  gsumzaddlem  17632  gsumzadd  17633  gsummptnn0fzfv  17695  dprdfadd  17731  subgdmdprd  17745  gsumdixp  17915  lspcl  18277  psrbaglesupp  18669  psrbaglefi  18673  resspsrmul  18718  evlslem4  18808  evlslem3  18814  fvcoe1  18877  psropprmul  18908  00ply1bas  18910  subrgvr1cl  18932  coe1mul2lem1  18937  coe1tmmul  18947  ply1coe  18966  ply1coeOLD  18967  evl1val  18994  evl1sca  18999  pf1const  19011  znunit  19211  frlmsslsp  19431  frlmup2  19434  lindfmm  19462  islindf4  19473  1mavmul  19650  mavmulass  19651  marepvcl  19671  1marepvmarrepid  19677  cramerimplem1  19785  pmatcollpw3fi1lem1  19887  pmatcollpw3fi1lem2  19888  cpmadugsumlemF  19977  cpmadugsumfi  19978  cayleyhamilton1  19993  hauscmplem  20498  ptbasid  20667  ptpjcn  20703  upxp  20715  uptx  20717  txcmplem2  20734  xkopt  20747  txhmeo  20895  alexsubALTlem3  21142  nrginvrcn  21772  nmoi  21811  nmoleub  21814  nmoiOLD  21827  nmoleubOLD  21830  cncfmet  22018  cnheibor  22061  evth  22065  pcopt  22131  pcopt2  22132  pcorevlem  22135  pi1xfrf  22162  pi1xfr  22164  pi1xfrcnvlem  22165  iscauf  22328  iscmet3lem1  22339  iscmet3lem2  22340  iscmet3  22341  causs  22346  bcthlem5  22374  bcth3  22377  ovolfcl  22497  ovolfioo  22498  ovolficc  22499  ovolficcss  22500  ovolfsval  22501  ovolmge0  22508  ovollb2lem  22519  ovolunlem1a  22527  ovoliunlem1  22533  ovoliunlem2  22534  ovoliun  22536  ovolicc1  22547  ovolicc2lem3  22550  ovolicc2lem4OLD  22551  ovolicc2lem4  22552  ovolicc2lem5  22553  voliunlem1  22582  volsup  22588  ioombl1lem2  22591  ovolfs2  22602  uniioovol  22615  uniiccvol  22616  uniioombllem3a  22621  uniioombllem3  22622  uniioombllem4  22623  uniioombllem5  22624  uniioombllem6  22625  dyadmbl  22637  volcn  22643  ismbf  22665  mbfadd  22696  mbfsub  22697  mbflimsup  22702  mbflimsupOLD  22703  0plef  22709  itg1climres  22751  mbfi1fseqlem1  22752  mbfi1fseqlem3  22754  mbfi1fseqlem4  22755  mbfi1fseqlem5  22756  mbfmul  22763  xrge0f  22768  itg2ge0  22772  itg2seq  22779  itg2uba  22780  itg2lea  22781  itg2eqa  22782  itg2splitlem  22785  itg2split  22786  itg2i1fseqle  22791  itg2i1fseq  22792  itg2i1fseq2  22793  itg2addlem  22795  bddmulibl  22875  ellimc3  22913  dvaddbr  22971  dvcobr  22979  dvcj  22983  dvfre  22984  dvcnvlem  23007  dvlip  23024  dvlipcn  23025  c1lip1  23028  tdeglem4  23088  tdeglem2  23089  coe1mul3  23127  ply1rem  23193  fta1g  23197  ig1pdvds  23207  ig1pdvdsOLD  23213  plyf  23231  plyeq0lem  23243  plypf1  23245  plyaddlem  23248  plymullem  23249  plyco  23274  dgreq  23277  0dgrb  23279  coefv0  23281  coeaddlem  23282  coemullem  23283  coemulc  23288  plycn  23294  dgrcolem2  23307  plycjlem  23309  plycj  23310  plyrecj  23312  plyreres  23315  dvply1  23316  vieta1lem2  23343  vieta1  23344  elqaalem2  23352  elqaalem2OLD  23355  aareccl  23361  aalioulem1  23367  ulmcaulem  23428  ulmcau  23429  ulmcn  23433  mtest  23438  psergf  23446  dvradcnv  23455  psercn2  23457  pserdvlem2  23462  pserdv2  23464  abelthlem6  23470  abelthlem8  23473  abelthlem9  23474  logtayl  23684  amgm  23995  ftalem1  24076  ftalem2  24077  ftalem3  24078  ftalem4  24079  ftalem5  24080  ftalem4OLD  24081  ftalem5OLD  24082  basellem2  24087  muinv  24201  dchrmulcl  24256  dchrinvcl  24260  dchrfi  24262  dchrghm  24263  dchrsum2  24275  dchrsum  24276  bposlem5  24295  lgscllem  24310  lgsval4a  24325  lgsneg  24326  lgsdir  24337  lgsdilem2  24338  lgsdi  24339  lgsne0  24340  lgseisenlem3  24358  rpvmasumlem  24404  dchrmusum2  24411  dchrvmasumiflem1  24418  dchrisum0ff  24424  dchrisum0flblem1  24425  dchrisum0fno1  24428  rpvmasum2  24429  dchrisum0re  24430  dchrisum0lem2a  24434  usgrarnedg  25190  usgraedg4  25193  usgrares1  25217  usgrwlknloop  25372  usgra2adedgwlkonALT  25423  usgra2wlkspthlem2  25427  cyclispthon  25440  fargshiftf  25443  usgrcyclnl2  25448  4cycl4dv  25474  el2wlkonotlem  25669  usg2wlkonot  25690  usg2wotspth  25691  vdgrnn0pnf  25716  frgrancvvdeqlemB  25845  ghgrplem2OLD  26176  lnoadd  26480  lnosub  26481  nmosetre  26486  nmooge0  26489  nmoub3i  26495  nmounbi  26498  phoeqi  26580  ubthlem1  26593  h2hcau  26713  h2hlm  26714  hoscl  27479  homcl  27480  hodcl  27481  hoaddcl  27492  homulcl  27493  homulid2  27534  homco1  27535  homulass  27536  hoadddi  27537  hoadddir  27538  hoeq1  27564  hoeq2  27565  adjsym  27567  nmopsetretALT  27597  nmfnsetre  27611  cnvadj  27626  hhcno  27638  hhcnf  27639  nmopub2tALT  27643  nmopge0  27645  unopf1o  27650  unoplin  27654  counop  27655  nmfnleub2  27660  nmfnge0  27661  hmoplin  27676  eigvalcl  27695  lnop0  27700  hmops  27754  hmopm  27755  nlelchi  27795  leop2  27858  leopadd  27866  leopmuli  27867  leopnmid  27872  hmopidmchi  27885  pjinvari  27925  sticl  27949  fcomptf  28335  rge0scvg  28829  esumcst  28958  esumfzf  28964  esumfsup  28965  esumfsupre  28966  hasheuni  28980  measdivcstOLD  29120  eulerpartlems  29266  eulerpartlemgc  29268  eulerpartlemb  29274  derangsn  29965  subfacp1lem5  29979  subfacp1lem6  29980  pconcon  30026  sconpi1  30034  txsconlem  30035  cvxscon  30038  cvmliftphtlem  30112  cvmlift3lem2  30115  cvmlift3lem4  30117  cvmlift3lem6  30119  elmrsubrn  30230  msubff  30240  msubvrs  30270  mclsssvlem  30272  ghomgrpilem2  30376  ghomcl  30382  ghomgsg  30383  faclim  30453  fprb  30484  soseq  30563  ptrecube  32004  heicant  32039  mblfinlem2  32042  itg2addnclem  32057  ftc1anclem1  32081  ftc1anclem2  32082  ftc1anclem4  32084  upixp  32120  fdc  32138  seqpo  32140  incsequz  32141  incsequz2  32142  metf1o  32148  geomcau  32152  sstotbnd2  32170  prdsbnd  32189  ismtyima  32199  ismtyhmeolem  32200  heiborlem3  32209  heiborlem6  32212  heiborlem10  32216  bfplem1  32218  ghomco  32245  mzpclall  35640  mzprename  35662  rexrabdioph  35708  rmydioph  35940  rmxdioph  35942  expdiophlem2  35948  expdioph  35949  pw2f1ocnv  35963  kelac1  35992  rngunsnply  36110  ofsubid  36743  ofdivrec  36745  ofdivcan4  36746  ofdivdiv2  36747  dvconstbi  36753  refsum2cnlem1  37421  dffo3f  37521  climinf  37781  climinfOLD  37782  stoweidlem26  37998  stoweidlem60  38033  stoweid  38037  dmvolsal  38317  caratheodory  38468  elhoi  38482  nnsum4primeseven  39040  nnsum4primesevenALTV  39041  2f1fvneq  39158  f1cofveqaeq  39159  1wlkpvtx  39857  1wlkepvtx  39858  1wlkres  39866  usgra2pthlem1  40175  mgmhmpropd  40293  rmsupp0  40661  domnmsuppn0  40662  gsumlsscl  40676  lincfsuppcl  40714  linccl  40715  lincdifsn  40725  lincsum  40730  lincscm  40731  lincscmcl  40733  lincext1  40755  lindslinindimp2lem1  40759  lindslinindimp2lem4  40762  lindslinindsimp2lem5  40763  snlindsntor  40772  lincresunitlem2  40777  lincresunit3lem1  40780  lincresunit3lem2  40781  lincresunit3  40782  lincreslvec3  40783  isldepslvec2  40786  zlmodzxzldeplem3  40803  aacllem  41046
  Copyright terms: Public domain W3C validator