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

Theorem ffvelrn 5931
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 5639 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 5930 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 469 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5645 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3416 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 463 . 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 367    e. wcel 1826   ran crn 4914    Fn wfn 5491   -->wf 5492   ` cfv 5496
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-fv 5504
This theorem is referenced by:  ffvelrni  5932  ffvelrnda  5933  dffo3  5948  foco2  5953  ffnfv  5959  ffvresb  5964  fcompt  5969  fsn2  5973  fvconst  5991  fcofo  6092  cocan1  6095  isocnv  6127  isocnv3  6129  isores2  6130  isopolem  6142  isosolem  6144  fovrn  6344  off  6453  fnwelem  6814  smofvon2  6945  smorndom  6957  omsmolem  7220  omsmo  7221  mapsncnv  7384  2dom  7507  xpdom2  7531  domunsncan  7536  xpmapenlem  7603  fiint  7712  ordiso2  7855  infdifsn  7987  cantnflem1  8021  cantnflem1OLD  8044  wemapwe  8052  wemapweOLD  8053  cnfcom3lem  8060  cnfcom3lemOLD  8068  fseqenlem1  8318  finacn  8344  ackbij1lem12  8524  cofsmo  8562  cfsmolem  8563  cfcoflem  8565  coftr  8566  isf32lem6  8651  isf32lem7  8652  isf34lem7  8672  isf34lem6  8673  acncc  8733  axdc2lem  8741  axdc3lem2  8744  axdc3lem4  8746  axdc4lem  8748  axcclem  8750  ttukeylem6  8807  alephreg  8870  pwcfsdom  8871  canthp1lem2  8942  canthp1  8943  pwfseqlem1  8947  pwfseqlem4a  8950  gruf  9100  fsequb2  11989  axdc4uzlem  11995  seqf1o  12051  hashf1lem1  12408  wwlktovf  12805  shftf  12914  limsupgre  13306  rlimuni  13375  lo1resb  13389  o1resb  13391  o1of2  13437  o1rlimmul  13443  isercolllem1  13489  isercolllem2  13490  isercolllem3  13491  isercoll  13492  climsup  13494  iseralt  13509  sumeq2ii  13517  summolem2a  13539  isumcl  13578  isumshft  13653  climcndslem2  13664  climcnds  13665  mertenslem2  13696  prodeq2ii  13722  prodmolem2a  13743  iprodcl  13796  rpnnen2lem10  13959  ruclem8  13972  ruclem12  13976  3dvds  14052  smueqlem  14142  nn0seqcvgd  14201  algrf  14204  eucalg  14218  phimullem  14311  pcmpt  14413  pcprod  14416  vdwlem11  14511  vdwnnlem3  14517  ramlb  14539  0ram  14540  ramcl  14549  imasaddfnlem  14935  imasaddflem  14937  mhmpropd  16089  ghmsub  16392  cntzmhm  16493  f1omvdconj  16588  pj1ghm  16838  gsumzaddlem  17051  gsumzadd  17052  gsumzaddlemOLD  17053  gsumzaddOLD  17054  gsummptnn0fzfv  17129  dprdfadd  17173  dprdfaddOLD  17180  subgdmdprd  17194  gsumdixpOLD  17370  gsumdixp  17371  lspcl  17735  psrbaglesupp  18130  psrbaglesuppOLD  18131  psrbaglefi  18136  psrbaglefiOLD  18137  resspsrmul  18185  evlslem4OLD  18286  evlslem4  18287  evlslem3  18296  fvcoe1  18359  psropprmul  18392  00ply1bas  18394  subrgvr1cl  18416  coe1mul2lem1  18421  coe1tmmul  18431  ply1coe  18450  ply1coeOLD  18451  evl1val  18478  evl1sca  18483  pf1const  18495  znunit  18693  frlmsslsp  18916  frlmup2  18919  lindfmm  18947  islindf4  18958  1mavmul  19135  mavmulass  19136  marepvcl  19156  1marepvmarrepid  19162  cramerimplem1  19270  pmatcollpw3fi1lem1  19372  pmatcollpw3fi1lem2  19373  cpmadugsumlemF  19462  cpmadugsumfi  19463  cayleyhamilton1  19478  hauscmplem  19992  ptbasid  20161  ptpjcn  20197  upxp  20209  uptx  20211  txcmplem2  20228  xkopt  20241  txhmeo  20389  alexsubALTlem3  20634  nrginvrcn  21285  nmoi  21320  nmoleub  21323  cncfmet  21497  cnheibor  21540  evth  21544  pcopt  21607  pcopt2  21608  pcorevlem  21611  pi1xfrf  21638  pi1xfr  21640  pi1xfrcnvlem  21641  iscauf  21804  iscmet3lem1  21815  iscmet3lem2  21816  iscmet3  21817  causs  21822  bcthlem5  21852  bcth3  21855  ovolfcl  21963  ovolfioo  21964  ovolficc  21965  ovolficcss  21966  ovolfsval  21967  ovolmge0  21973  ovollb2lem  21984  ovolunlem1a  21992  ovoliunlem1  21998  ovoliunlem2  21999  ovoliun  22001  ovolicc1  22012  ovolicc2lem3  22015  ovolicc2lem4  22016  ovolicc2lem5  22017  voliunlem1  22045  volsup  22051  ioombl1lem2  22054  ovolfs2  22065  uniioovol  22073  uniiccvol  22074  uniioombllem3a  22078  uniioombllem3  22079  uniioombllem4  22080  uniioombllem5  22081  uniioombllem6  22082  dyadmbl  22094  volcn  22100  ismbf  22122  mbfadd  22153  mbfsub  22154  mbflimsup  22158  0plef  22164  itg1climres  22206  mbfi1fseqlem1  22207  mbfi1fseqlem3  22209  mbfi1fseqlem4  22210  mbfi1fseqlem5  22211  mbfmul  22218  xrge0f  22223  itg2ge0  22227  itg2seq  22234  itg2uba  22235  itg2lea  22236  itg2eqa  22237  itg2splitlem  22240  itg2split  22241  itg2i1fseqle  22246  itg2i1fseq  22247  itg2i1fseq2  22248  itg2addlem  22250  bddmulibl  22330  ellimc3  22368  dvaddbr  22426  dvcobr  22434  dvcj  22438  dvfre  22439  dvcnvlem  22462  dvlip  22479  dvlipcn  22480  c1lip1  22483  tdeglem4  22543  tdeglem2  22544  coe1mul3  22585  ply1rem  22649  fta1g  22653  ig1pdvds  22662  plyf  22680  plyeq0lem  22692  plypf1  22694  plyaddlem  22697  plymullem  22698  plyco  22723  dgreq  22726  0dgrb  22728  coefv0  22730  coeaddlem  22731  coemullem  22732  coemulc  22737  plycn  22743  dgrcolem2  22756  plycjlem  22758  plycj  22759  plyrecj  22761  plyreres  22764  dvply1  22765  vieta1lem2  22792  vieta1  22793  elqaalem2  22801  aareccl  22807  aalioulem1  22813  ulmcaulem  22874  ulmcau  22875  ulmcn  22879  mtest  22884  psergf  22892  dvradcnv  22901  psercn2  22903  pserdvlem2  22908  pserdv2  22910  abelthlem6  22916  abelthlem8  22919  abelthlem9  22920  logtayl  23128  amgm  23437  ftalem1  23463  ftalem2  23464  ftalem3  23465  ftalem4  23466  ftalem5  23467  basellem2  23472  muinv  23586  dchrmulcl  23641  dchrinvcl  23645  dchrfi  23647  dchrghm  23648  dchrsum2  23660  dchrsum  23661  bposlem5  23680  lgscllem  23695  lgsval4a  23710  lgsneg  23711  lgsdir  23722  lgsdilem2  23723  lgsdi  23724  lgsne0  23725  lgseisenlem3  23743  rpvmasumlem  23789  dchrmusum2  23796  dchrvmasumiflem1  23803  dchrisum0ff  23809  dchrisum0flblem1  23810  dchrisum0fno1  23813  rpvmasum2  23814  dchrisum0re  23815  dchrisum0lem2a  23819  usgrarnedg  24505  usgraedg4  24508  usgrares1  24531  usgrnloop  24686  usgra2adedgwlkonALT  24737  usgra2wlkspthlem2  24741  cyclispthon  24754  fargshiftf  24757  usgrcyclnl2  24762  4cycl4dv  24788  el2wlkonotlem  24983  usg2wlkonot  25004  usg2wotspth  25005  vdgrnn0pnf  25030  frgrancvvdeqlemB  25159  ghgrplem2OLD  25486  lnoadd  25790  lnosub  25791  nmosetre  25796  nmooge0  25799  nmoub3i  25805  nmounbi  25808  phoeqi  25890  ubthlem1  25903  h2hcau  26013  h2hlm  26014  hoscl  26780  homcl  26781  hodcl  26782  hoaddcl  26793  homulcl  26794  homulid2  26835  homco1  26836  homulass  26837  hoadddi  26838  hoadddir  26839  hoeq1  26865  hoeq2  26866  adjsym  26868  nmopsetretALT  26898  nmfnsetre  26912  cnvadj  26927  hhcno  26939  hhcnf  26940  nmopub2tALT  26944  nmopge0  26946  unopf1o  26951  unoplin  26955  counop  26956  nmfnleub2  26961  nmfnge0  26962  hmoplin  26977  eigvalcl  26996  lnop0  27001  hmops  27055  hmopm  27056  nlelchi  27096  leop2  27159  leopadd  27167  leopmuli  27168  leopnmid  27173  hmopidmchi  27186  pjinvari  27226  sticl  27250  fcomptf  27644  rge0scvg  28085  esumcst  28211  esumfzf  28217  esumfsup  28218  esumfsupre  28219  hasheuni  28233  measdivcstOLD  28351  eulerpartlems  28482  eulerpartlemgc  28484  eulerpartlemb  28490  derangsn  28803  subfacp1lem5  28817  subfacp1lem6  28818  pconcon  28865  sconpi1  28873  txsconlem  28874  cvxscon  28877  cvmliftphtlem  28951  cvmlift3lem2  28954  cvmlift3lem4  28956  cvmlift3lem6  28958  elmrsubrn  29069  msubff  29079  msubvrs  29109  mclsssvlem  29111  ghomgrpilem2  29215  ghomcl  29221  ghomgsg  29222  faclim  29337  fprb  29368  soseq  29499  heicant  30214  mblfinlem2  30217  itg2addnclem  30232  ftc1anclem1  30256  ftc1anclem2  30257  ftc1anclem4  30259  upixp  30386  fdc  30404  seqpo  30406  incsequz  30407  incsequz2  30408  metf1o  30414  geomcau  30418  sstotbnd2  30436  prdsbnd  30455  ismtyima  30465  ismtyhmeolem  30466  heiborlem3  30475  heiborlem6  30478  heiborlem10  30482  bfplem1  30484  ghomco  30511  mzpclall  30825  mzprename  30847  rexrabdioph  30893  rmydioph  31122  rmxdioph  31124  expdiophlem2  31130  expdioph  31131  pw2f1ocnv  31145  kelac1  31175  rngunsnply  31290  ofsubid  31397  ofdivrec  31399  ofdivcan4  31400  ofdivdiv2  31401  dvconstbi  31407  refsum2cnlem1  31579  climinf  31778  stoweidlem26  31974  stoweidlem60  32008  stoweid  32011  2f1fvneq  32628  usgra2pthlem1  32671  mgmhmpropd  32791  rmsupp0  33161  domnmsuppn0  33162  gsumlsscl  33176  lincfsuppcl  33214  linccl  33215  lincdifsn  33225  lincsum  33230  lincscm  33231  lincscmcl  33233  lincext1  33255  lindslinindimp2lem1  33259  lindslinindimp2lem4  33262  lindslinindsimp2lem5  33263  snlindsntor  33272  lincresunitlem2  33277  lincresunit3lem1  33280  lincresunit3lem2  33281  lincresunit3  33282  lincreslvec3  33283  isldepslvec2  33286  zlmodzxzldeplem3  33303  aacllem  33550
  Copyright terms: Public domain W3C validator