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

Theorem ffvelrn 6010
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 5717 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 6009 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 471 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5723 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3485 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 465 . 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 369    e. wcel 1802   ran crn 4986    Fn wfn 5569   -->wf 5570   ` cfv 5574
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-fv 5582
This theorem is referenced by:  ffvelrni  6011  ffvelrnda  6012  dffo3  6027  foco2  6032  ffnfv  6038  ffvresb  6043  fcompt  6048  fsn2  6052  fvconst  6070  fcofo  6172  cocan1  6175  isocnv  6207  isocnv3  6209  isores2  6210  isopolem  6222  isosolem  6224  fovrn  6426  off  6535  fnwelem  6896  smofvon2  7025  smorndom  7037  omsmolem  7300  omsmo  7301  mapsncnv  7463  2dom  7586  xpdom2  7610  domunsncan  7615  xpmapenlem  7682  fiint  7795  ordiso2  7938  infdifsn  8071  cantnflem1  8106  cantnflem1OLD  8129  wemapwe  8137  wemapweOLD  8138  cnfcom3lem  8145  cnfcom3lemOLD  8153  fseqenlem1  8403  finacn  8429  ackbij1lem12  8609  cofsmo  8647  cfsmolem  8648  cfcoflem  8650  coftr  8651  isf32lem6  8736  isf32lem7  8737  isf34lem7  8757  isf34lem6  8758  acncc  8818  axdc2lem  8826  axdc3lem2  8829  axdc3lem4  8831  axdc4lem  8833  axcclem  8835  ttukeylem6  8892  alephreg  8955  pwcfsdom  8956  canthp1lem2  9029  canthp1  9030  pwfseqlem1  9034  pwfseqlem4a  9037  gruf  9187  fsequb2  12060  axdc4uzlem  12066  seqf1o  12122  hashf1lem1  12478  eqs1  12595  wwlktovf  12868  shftf  12886  limsupgre  13278  rlimuni  13347  lo1resb  13361  o1resb  13363  o1of2  13409  o1rlimmul  13415  isercolllem1  13461  isercolllem2  13462  isercolllem3  13463  isercoll  13464  climsup  13466  iseralt  13481  sumeq2ii  13489  summolem2a  13511  isumcl  13550  isumshft  13625  climcndslem2  13636  climcnds  13637  mertenslem2  13668  rpnnen2lem10  13829  ruclem8  13842  ruclem12  13846  3dvds  13922  smueqlem  14012  nn0seqcvgd  14071  algrf  14074  eucalg  14088  phimullem  14181  pcmpt  14283  pcprod  14286  vdwlem11  14381  vdwnnlem3  14387  ramlb  14409  0ram  14410  ramcl  14419  imasaddfnlem  14797  imasaddflem  14799  mhmpropd  15841  ghmsub  16144  cntzmhm  16245  f1omvdconj  16340  pj1ghm  16590  gsumzaddlem  16803  gsumzadd  16804  gsumzaddlemOLD  16805  gsumzaddOLD  16806  gsummptnn0fzfv  16885  dprdfadd  16928  dprdfaddOLD  16935  subgdmdprd  16949  gsumdixpOLD  17125  gsumdixp  17126  lspcl  17490  psrbaglesupp  17885  psrbaglesuppOLD  17886  psrbaglefi  17891  psrbaglefiOLD  17892  resspsrmul  17940  evlslem4OLD  18041  evlslem4  18042  evlslem3  18051  fvcoe1  18114  psropprmul  18147  00ply1bas  18149  subrgvr1cl  18171  coe1mul2lem1  18176  coe1tmmul  18186  ply1coe  18205  ply1coeOLD  18206  evl1val  18233  evl1sca  18238  pf1const  18250  znunit  18469  frlmsslsp  18696  frlmsslspOLD  18697  frlmup2  18700  lindfmm  18729  islindf4  18740  1mavmul  18917  mavmulass  18918  marepvcl  18938  1marepvmarrepid  18944  cramerimplem1  19052  pmatcollpw3fi1lem1  19154  pmatcollpw3fi1lem2  19155  cpmadugsumlemF  19244  cpmadugsumfi  19245  cayleyhamilton1  19260  hauscmplem  19772  ptbasid  19942  ptpjcn  19978  upxp  19990  uptx  19992  txcmplem2  20009  xkopt  20022  txhmeo  20170  alexsubALTlem3  20415  nrginvrcn  21066  nmoi  21101  nmoleub  21104  cncfmet  21278  cnheibor  21321  evth  21325  pcopt  21388  pcopt2  21389  pcorevlem  21392  pi1xfrf  21419  pi1xfr  21421  pi1xfrcnvlem  21422  iscauf  21585  iscmet3lem1  21596  iscmet3lem2  21597  iscmet3  21598  causs  21603  bcthlem5  21633  bcth3  21636  ovolfcl  21744  ovolfioo  21745  ovolficc  21746  ovolficcss  21747  ovolfsval  21748  ovolmge0  21754  ovollb2lem  21765  ovolunlem1a  21773  ovoliunlem1  21779  ovoliunlem2  21780  ovoliun  21782  ovolicc1  21793  ovolicc2lem3  21796  ovolicc2lem4  21797  ovolicc2lem5  21798  voliunlem1  21826  volsup  21832  ioombl1lem2  21835  ovolfs2  21846  uniioovol  21854  uniiccvol  21855  uniioombllem3a  21859  uniioombllem3  21860  uniioombllem4  21861  uniioombllem5  21862  uniioombllem6  21863  dyadmbl  21875  volcn  21881  ismbf  21903  mbfadd  21934  mbfsub  21935  mbflimsup  21939  0plef  21945  itg1climres  21987  mbfi1fseqlem1  21988  mbfi1fseqlem3  21990  mbfi1fseqlem4  21991  mbfi1fseqlem5  21992  mbfmul  21999  xrge0f  22004  itg2ge0  22008  itg2seq  22015  itg2uba  22016  itg2lea  22017  itg2eqa  22018  itg2splitlem  22021  itg2split  22022  itg2i1fseqle  22027  itg2i1fseq  22028  itg2i1fseq2  22029  itg2addlem  22031  bddmulibl  22111  ellimc3  22149  dvaddbr  22207  dvcobr  22215  dvcj  22219  dvfre  22220  dvcnvlem  22243  dvlip  22260  dvlipcn  22261  c1lip1  22264  tdeglem4  22324  tdeglem2  22325  coe1mul3  22366  ply1rem  22430  fta1g  22434  ig1pdvds  22443  plyf  22461  plyeq0lem  22473  plypf1  22475  plyaddlem  22478  plymullem  22479  plyco  22504  dgreq  22507  0dgrb  22509  coefv0  22510  coeaddlem  22511  coemullem  22512  coemulc  22517  plycn  22523  dgrcolem2  22536  plycjlem  22538  plycj  22539  plyrecj  22541  plyreres  22544  dvply1  22545  vieta1lem2  22572  vieta1  22573  elqaalem2  22581  aareccl  22587  aalioulem1  22593  ulmcaulem  22654  ulmcau  22655  ulmcn  22659  mtest  22664  psergf  22672  dvradcnv  22681  psercn2  22683  pserdvlem2  22688  pserdv2  22690  abelthlem6  22696  abelthlem8  22699  abelthlem9  22700  logtayl  22906  amgm  23185  ftalem1  23211  ftalem2  23212  ftalem3  23213  ftalem4  23214  ftalem5  23215  basellem2  23220  muinv  23334  dchrmulcl  23389  dchrinvcl  23393  dchrfi  23395  dchrghm  23396  dchrsum2  23408  dchrsum  23409  bposlem5  23428  lgscllem  23443  lgsval4a  23458  lgsneg  23459  lgsdir  23470  lgsdilem2  23471  lgsdi  23472  lgsne0  23473  lgseisenlem3  23491  rpvmasumlem  23537  dchrmusum2  23544  dchrvmasumiflem1  23551  dchrisum0ff  23557  dchrisum0flblem1  23558  dchrisum0fno1  23561  rpvmasum2  23562  dchrisum0re  23563  dchrisum0lem2a  23567  usgrarnedg  24249  usgraedg4  24252  usgrares1  24275  usgrnloop  24430  usgra2adedgwlkonALT  24481  usgra2wlkspthlem2  24485  cyclispthon  24498  fargshiftf  24501  usgrcyclnl2  24506  4cycl4dv  24532  el2wlkonotlem  24727  usg2wlkonot  24748  usg2wotspth  24749  vdgrnn0pnf  24774  frgrancvvdeqlemB  24903  ghgrplem2OLD  25234  lnoadd  25538  lnosub  25539  nmosetre  25544  nmooge0  25547  nmoub3i  25553  nmounbi  25556  phoeqi  25638  ubthlem1  25651  h2hcau  25761  h2hlm  25762  hoscl  26529  homcl  26530  hodcl  26531  hoaddcl  26542  homulcl  26543  homulid2  26584  homco1  26585  homulass  26586  hoadddi  26587  hoadddir  26588  hoeq1  26614  hoeq2  26615  adjsym  26617  nmopsetretALT  26647  nmfnsetre  26661  cnvadj  26676  hhcno  26688  hhcnf  26689  nmopub2tALT  26693  nmopge0  26695  unopf1o  26700  unoplin  26704  counop  26705  nmfnleub2  26710  nmfnge0  26711  hmoplin  26726  eigvalcl  26745  lnop0  26750  hmops  26804  hmopm  26805  nlelchi  26845  leop2  26908  leopadd  26916  leopmuli  26917  leopnmid  26922  hmopidmchi  26935  pjinvari  26975  sticl  26999  fcomptf  27368  rge0scvg  27797  esumcst  27937  esumfzf  27941  esumfsup  27942  esumfsupre  27943  hasheuni  27957  measdivcstOLD  28061  eulerpartlems  28165  eulerpartlemgc  28167  eulerpartlemb  28173  derangsn  28480  subfacp1lem5  28494  subfacp1lem6  28495  pconcon  28542  sconpi1  28550  txsconlem  28551  cvxscon  28554  cvmliftphtlem  28628  cvmlift3lem2  28631  cvmlift3lem4  28633  cvmlift3lem6  28635  elmrsubrn  28746  msubff  28756  msubvrs  28786  mclsssvlem  28788  ghomgrpilem2  28892  ghomcl  28898  ghomgsg  28899  prodeq2ii  29013  prodmolem2a  29034  iprodcl  29088  faclim  29139  fprb  29171  soseq  29302  heicant  30017  mblfinlem2  30020  itg2addnclem  30034  ftc1anclem1  30058  ftc1anclem2  30059  ftc1anclem4  30061  upixp  30188  fdc  30206  seqpo  30208  incsequz  30209  incsequz2  30210  metf1o  30216  geomcau  30220  sstotbnd2  30238  prdsbnd  30257  ismtyima  30267  ismtyhmeolem  30268  heiborlem3  30277  heiborlem6  30280  heiborlem10  30284  bfplem1  30286  ghomco  30313  mzpclall  30627  mzprename  30650  rexrabdioph  30695  rmydioph  30924  rmxdioph  30926  expdiophlem2  30932  expdioph  30933  pw2f1ocnv  30947  kelac1  30977  rngunsnply  31091  ofsubid  31198  ofdivrec  31200  ofdivcan4  31201  ofdivdiv2  31202  dvconstbi  31208  refsum2cnlem1  31359  climinf  31516  stoweidlem26  31693  stoweidlem60  31727  stoweid  31730  2f1fvneq  32141  usgra2pthlem1  32187  mgmhmpropd  32307  rmsupp0  32671  domnmsuppn0  32672  gsumlsscl  32686  lincfsuppcl  32724  linccl  32725  lincdifsn  32735  lincsum  32740  lincscm  32741  lincscmcl  32743  lincext1  32765  lindslinindimp2lem1  32769  lindslinindimp2lem4  32772  lindslinindsimp2lem5  32773  snlindsntor  32782  lincresunitlem2  32787  lincresunit3lem1  32790  lincresunit3lem2  32791  lincresunit3  32792  lincreslvec3  32793  isldepslvec2  32796  zlmodzxzldeplem3  32813
  Copyright terms: Public domain W3C validator