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 5722 . . 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 5728 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3496 . . 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 1762   ran crn 4993    Fn wfn 5574   -->wf 5575   ` cfv 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-fv 5587
This theorem is referenced by:  ffvelrni  6011  ffvelrnda  6012  dffo3  6027  foco2  6032  ffnfv  6038  ffvresb  6043  fcompt  6048  fsn2  6052  fvconst  6070  fcofo  6170  cocan1  6173  isocnv  6205  isocnv3  6207  isores2  6208  isopolem  6220  isosolem  6222  fovrn  6420  off  6529  fnwelem  6888  smofvon2  7017  smorndom  7029  omsmolem  7292  omsmo  7293  mapsncnv  7455  2dom  7578  xpdom2  7602  domunsncan  7607  xpmapenlem  7674  fiint  7786  ordiso2  7929  infdifsn  8062  cantnflem1  8097  cantnflem1OLD  8120  wemapwe  8128  wemapweOLD  8129  cnfcom3lem  8136  cnfcom3lemOLD  8144  fseqenlem1  8394  finacn  8420  ackbij1lem12  8600  cofsmo  8638  cfsmolem  8639  cfcoflem  8641  coftr  8642  isf32lem6  8727  isf32lem7  8728  isf34lem7  8748  isf34lem6  8749  acncc  8809  axdc2lem  8817  axdc3lem2  8820  axdc3lem4  8822  axdc4lem  8824  axcclem  8826  ttukeylem6  8883  alephreg  8946  pwcfsdom  8947  canthp1lem2  9020  canthp1  9021  pwfseqlem1  9025  pwfseqlem4a  9028  gruf  9178  fsequb2  12042  axdc4uzlem  12048  seqf1o  12104  hashf1lem1  12457  eqs1  12571  wwlktovf  12844  shftf  12862  limsupgre  13253  rlimuni  13322  lo1resb  13336  o1resb  13338  o1of2  13384  o1rlimmul  13390  isercolllem1  13436  isercolllem2  13437  isercolllem3  13438  isercoll  13439  climsup  13441  iseralt  13456  sumeq2ii  13464  summolem2a  13486  isumcl  13525  isumshft  13603  climcndslem2  13614  climcnds  13615  mertenslem2  13646  rpnnen2lem10  13807  ruclem8  13820  ruclem12  13824  3dvds  13898  smueqlem  13988  nn0seqcvgd  14047  algrf  14050  eucalg  14064  phimullem  14157  pcmpt  14259  pcprod  14262  vdwlem11  14357  vdwnnlem3  14363  ramlb  14385  0ram  14386  ramcl  14395  imasaddfnlem  14772  imasaddflem  14774  mhmpropd  15776  ghmsub  16063  cntzmhm  16164  f1omvdconj  16260  pj1ghm  16510  gsumzaddlem  16718  gsumzadd  16719  gsumzaddlemOLD  16720  gsumzaddOLD  16721  gsummptnn0fzfv  16800  dprdfadd  16843  dprdfaddOLD  16850  dprdf1o  16862  subgdmdprd  16864  gsumdixpOLD  17034  gsumdixp  17035  lspcl  17398  psrbaglesupp  17781  psrbaglesuppOLD  17782  psrbaglefi  17787  psrbaglefiOLD  17788  resspsrmul  17836  evlslem4OLD  17937  evlslem4  17938  evlslem3  17947  fvcoe1  18010  psropprmul  18043  00ply1bas  18045  subrgvr1cl  18067  coe1mul2lem1  18072  coe1tmmul  18082  ply1coe  18101  ply1coeOLD  18102  evl1val  18129  evl1sca  18134  pf1const  18146  znunit  18362  frlmsslsp  18589  frlmsslspOLD  18590  frlmup2  18593  lindfmm  18622  islindf4  18633  1mavmul  18810  mavmulass  18811  marepvcl  18831  1marepvmarrepid  18837  cramerimplem1  18945  pmatcollpw3fi1lem1  19047  pmatcollpw3fi1lem2  19048  cpmadugsumlemF  19137  cpmadugsumfi  19138  cayleyhamilton1  19153  hauscmplem  19665  ptbasid  19804  ptpjcn  19840  upxp  19852  uptx  19854  txcmplem2  19871  xkopt  19884  txhmeo  20032  alexsubALTlem3  20277  nrginvrcn  20928  nmoi  20963  nmoleub  20966  cncfmet  21140  cnheibor  21183  evth  21187  pcopt  21250  pcopt2  21251  pcorevlem  21254  pi1xfrf  21281  pi1xfr  21283  pi1xfrcnvlem  21284  iscauf  21447  iscmet3lem1  21458  iscmet3lem2  21459  iscmet3  21460  causs  21465  bcthlem5  21495  bcth3  21498  ovolfcl  21606  ovolfioo  21607  ovolficc  21608  ovolficcss  21609  ovolfsval  21610  ovolmge0  21616  ovollb2lem  21627  ovolunlem1a  21635  ovoliunlem1  21641  ovoliunlem2  21642  ovoliun  21644  ovolicc1  21655  ovolicc2lem3  21658  ovolicc2lem4  21659  ovolicc2lem5  21660  voliunlem1  21688  volsup  21694  ioombl1lem2  21697  ovolfs2  21708  uniioovol  21716  uniiccvol  21717  uniioombllem3a  21721  uniioombllem3  21722  uniioombllem4  21723  uniioombllem5  21724  uniioombllem6  21725  dyadmbl  21737  volcn  21743  ismbf  21765  mbfadd  21796  mbfsub  21797  mbflimsup  21801  0plef  21807  itg1climres  21849  mbfi1fseqlem1  21850  mbfi1fseqlem3  21852  mbfi1fseqlem4  21853  mbfi1fseqlem5  21854  mbfmul  21861  xrge0f  21866  itg2ge0  21870  itg2seq  21877  itg2uba  21878  itg2lea  21879  itg2eqa  21880  itg2splitlem  21883  itg2split  21884  itg2i1fseqle  21889  itg2i1fseq  21890  itg2i1fseq2  21891  itg2addlem  21893  bddmulibl  21973  ellimc3  22011  dvaddbr  22069  dvcobr  22077  dvcj  22081  dvfre  22082  dvcnvlem  22105  dvlip  22122  dvlipcn  22123  c1lip1  22126  tdeglem4  22186  tdeglem2  22187  coe1mul3  22228  ply1rem  22292  fta1g  22296  ig1pdvds  22305  plyf  22323  plyeq0lem  22335  plypf1  22337  plyaddlem  22340  plymullem  22341  plyco  22366  dgreq  22369  0dgrb  22371  coefv0  22372  coeaddlem  22373  coemullem  22374  coemulc  22379  plycn  22385  dgrcolem2  22398  plycjlem  22400  plycj  22401  plyrecj  22403  plyreres  22406  dvply1  22407  vieta1lem2  22434  vieta1  22435  elqaalem2  22443  aareccl  22449  aalioulem1  22455  ulmcaulem  22516  ulmcau  22517  ulmcn  22521  mtest  22526  psergf  22534  dvradcnv  22543  psercn2  22545  pserdvlem2  22550  pserdv2  22552  abelthlem6  22558  abelthlem8  22561  abelthlem9  22562  logtayl  22762  amgm  23041  ftalem1  23067  ftalem2  23068  ftalem3  23069  ftalem4  23070  ftalem5  23071  basellem2  23076  muinv  23190  dchrmulcl  23245  dchrinvcl  23249  dchrfi  23251  dchrghm  23252  dchrsum2  23264  dchrsum  23265  bposlem5  23284  lgscllem  23299  lgsval4a  23314  lgsneg  23315  lgsdir  23326  lgsdilem2  23327  lgsdi  23328  lgsne0  23329  lgseisenlem3  23347  rpvmasumlem  23393  dchrmusum2  23400  dchrvmasumiflem1  23407  dchrisum0ff  23413  dchrisum0flblem1  23414  dchrisum0fno1  23417  rpvmasum2  23418  dchrisum0re  23419  dchrisum0lem2a  23423  usgrarnedg  24046  usgraedg4  24049  usgrares1  24072  usgrnloop  24227  usgra2adedgwlkonALT  24278  usgra2wlkspthlem2  24282  cyclispthon  24295  fargshiftf  24298  usgrcyclnl2  24303  4cycl4dv  24329  el2wlkonotlem  24524  usg2wlkonot  24545  usg2wotspth  24546  vdgrnn0pnf  24571  ghgrplem2  24895  lnoadd  25199  lnosub  25200  nmosetre  25205  nmooge0  25208  nmoub3i  25214  nmounbi  25217  phoeqi  25299  ubthlem1  25312  h2hcau  25422  h2hlm  25423  hoscl  26190  homcl  26191  hodcl  26192  hoaddcl  26203  homulcl  26204  homulid2  26245  homco1  26246  homulass  26247  hoadddi  26248  hoadddir  26249  hoeq1  26275  hoeq2  26276  adjsym  26278  nmopsetretALT  26308  nmfnsetre  26322  cnvadj  26337  hhcno  26349  hhcnf  26350  nmopub2tALT  26354  nmopge0  26356  unopf1o  26361  unoplin  26365  counop  26366  nmfnleub2  26371  nmfnge0  26372  hmoplin  26387  eigvalcl  26406  lnop0  26411  hmops  26465  hmopm  26466  nlelchi  26506  leop2  26569  leopadd  26577  leopmuli  26578  leopnmid  26583  hmopidmchi  26596  pjinvari  26636  sticl  26660  fcomptf  27025  rge0scvg  27417  esumcst  27561  esumfzf  27565  esumfsup  27566  esumfsupre  27567  hasheuni  27581  measdivcstOLD  27685  eulerpartlems  27789  eulerpartlemgc  27791  eulerpartlemb  27797  derangsn  28104  subfacp1lem5  28118  subfacp1lem6  28119  pconcon  28166  sconpi1  28174  txsconlem  28175  cvxscon  28178  cvmliftphtlem  28252  cvmlift3lem2  28255  cvmlift3lem4  28257  cvmlift3lem6  28259  ghomgrpilem2  28351  ghomcl  28357  ghomgsg  28358  prodeq2ii  28472  prodmolem2a  28493  iprodcl  28547  faclim  28598  fprb  28630  soseq  28761  heicant  29477  mblfinlem2  29480  itg2addnclem  29494  ftc1anclem1  29518  ftc1anclem2  29519  ftc1anclem4  29521  upixp  29674  fdc  29692  seqpo  29694  incsequz  29695  incsequz2  29696  metf1o  29702  geomcau  29706  sstotbnd2  29724  prdsbnd  29743  ismtyima  29753  ismtyhmeolem  29754  heiborlem3  29763  heiborlem6  29766  heiborlem10  29770  bfplem1  29772  ghomco  29799  mzpclall  30114  mzprename  30137  rexrabdioph  30182  rmydioph  30413  rmxdioph  30415  expdiophlem2  30421  expdioph  30422  pw2f1ocnv  30436  kelac1  30466  rngunsnply  30580  ofsubid  30648  ofdivrec  30650  ofdivcan4  30651  ofdivdiv2  30652  dvconstbi  30658  refsum2cnlem1  30809  climinf  30967  icccncfext  31045  itgspltprt  31116  itgiccshift  31117  itgperiod  31118  itgsbtaddcnst  31119  stoweidlem26  31145  stoweidlem60  31179  stoweid  31182  dirkercncflem2  31223  fourierdlem1  31227  fourierdlem93  31319  fourierdlem101  31327  fourierdlem111  31337  2f1fvneq  31595  usgra2pthlem1  31641  frgrancvvdeqlemB  31757  rmsupp0  31909  domnmsuppn0  31910  gsumlsscl  31924  lincfsuppcl  31962  linccl  31963  lincdifsn  31973  lincsum  31978  lincscm  31979  lincscmcl  31981  lincext1  32003  lindslinindimp2lem1  32007  lindslinindimp2lem4  32010  lindslinindsimp2lem5  32011  snlindsntor  32020  lincresunitlem2  32025  lincresunit3lem1  32028  lincresunit3lem2  32029  lincresunit3  32030  lincreslvec3  32031  isldepslvec2  32034  zlmodzxzldeplem3  32059
  Copyright terms: Public domain W3C validator