MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ffvelrn Structured 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 5746 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 6034 . . 3  |-  ( ( F  Fn  A  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
31, 2sylan 473 . 2  |-  ( ( F : A --> B  /\  C  e.  A )  ->  ( F `  C
)  e.  ran  F
)
4 frn 5752 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3463 . . 3  |-  ( F : A --> B  -> 
( ( F `  C )  e.  ran  F  ->  ( F `  C )  e.  B
) )
65adantr 466 . 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 370    e. wcel 1872   ran crn 4854    Fn wfn 5596   -->wf 5597   ` cfv 5601
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-id 4768  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-fv 5609
This theorem is referenced by:  ffvelrni  6036  ffvelrnda  6037  dffo3  6052  foco2  6057  ffnfv  6064  ffvresb  6069  fcompt  6074  fsn2  6077  fvconst  6097  fcofo  6201  cocan1  6204  isocnv  6236  isocnv3  6238  isores2  6239  isopolem  6251  isosolem  6253  fovrn  6453  off  6560  fnwelem  6922  smofvon2  7086  smorndom  7098  omsmolem  7365  omsmo  7366  mapsncnv  7529  2dom  7652  xpdom2  7676  domunsncan  7681  xpmapenlem  7748  fiint  7857  ordiso2  8039  infdifsn  8170  cantnflem1  8202  wemapwe  8210  cnfcom3lem  8216  fseqenlem1  8462  finacn  8488  ackbij1lem12  8668  cofsmo  8706  cfsmolem  8707  cfcoflem  8709  coftr  8710  isf32lem6  8795  isf32lem7  8796  isf34lem7  8816  isf34lem6  8817  acncc  8877  axdc2lem  8885  axdc3lem2  8888  axdc3lem4  8890  axdc4lem  8892  axcclem  8894  ttukeylem6  8951  alephreg  9014  pwcfsdom  9015  canthp1lem2  9085  canthp1  9086  pwfseqlem1  9090  pwfseqlem4a  9093  gruf  9243  fsequb2  12195  axdc4uzlem  12201  seqf1o  12260  hashf1lem1  12622  wwlktovf  13031  shftf  13142  limsupgre  13541  limsupgreOLD  13542  rlimuni  13613  lo1resb  13627  o1resb  13629  o1of2  13675  o1rlimmul  13681  isercolllem1  13727  isercolllem2  13728  isercolllem3  13729  isercoll  13730  climsup  13732  iseralt  13750  sumeq2ii  13758  summolem2a  13780  isumcl  13821  isumshft  13896  climcndslem2  13907  climcnds  13908  mertenslem2  13940  prodeq2ii  13966  prodmolem2a  13987  iprodcl  14053  rpnnen2lem10  14275  ruclem8  14288  ruclem12  14292  3dvds  14368  smueqlem  14463  nn0seqcvgd  14528  algrf  14531  eucalg  14545  phimullem  14726  pcmpt  14836  pcprod  14839  vdwlem11  14940  vdwnnlem3  14946  ramlb  14976  0ram  14977  ramcl  14986  prmgaplcmlem1OLD  15011  prmgaplcmlem2OLD  15012  prmdvdsprmorpOLD  15015  prmgapprmorlemOLD  15016  prmorlelcmfOLD  15019  prmorlelcmsOLDOLD  15021  prmgaplem8  15027  imasaddfnlem  15433  imasaddflem  15435  mhmpropd  16587  ghmsub  16890  cntzmhm  16991  f1omvdconj  17086  pj1ghm  17352  gsumzaddlem  17553  gsumzadd  17554  gsummptnn0fzfv  17616  dprdfadd  17652  subgdmdprd  17666  gsumdixp  17836  lspcl  18198  psrbaglesupp  18591  psrbaglefi  18595  resspsrmul  18640  evlslem4  18730  evlslem3  18736  fvcoe1  18799  psropprmul  18830  00ply1bas  18832  subrgvr1cl  18854  coe1mul2lem1  18859  coe1tmmul  18869  ply1coe  18888  ply1coeOLD  18889  evl1val  18916  evl1sca  18921  pf1const  18933  znunit  19132  frlmsslsp  19352  frlmup2  19355  lindfmm  19383  islindf4  19394  1mavmul  19571  mavmulass  19572  marepvcl  19592  1marepvmarrepid  19598  cramerimplem1  19706  pmatcollpw3fi1lem1  19808  pmatcollpw3fi1lem2  19809  cpmadugsumlemF  19898  cpmadugsumfi  19899  cayleyhamilton1  19914  hauscmplem  20419  ptbasid  20588  ptpjcn  20624  upxp  20636  uptx  20638  txcmplem2  20655  xkopt  20668  txhmeo  20816  alexsubALTlem3  21062  nrginvrcn  21692  nmoi  21731  nmoleub  21734  nmoiOLD  21747  nmoleubOLD  21750  cncfmet  21938  cnheibor  21981  evth  21985  pcopt  22051  pcopt2  22052  pcorevlem  22055  pi1xfrf  22082  pi1xfr  22084  pi1xfrcnvlem  22085  iscauf  22248  iscmet3lem1  22259  iscmet3lem2  22260  iscmet3  22261  causs  22266  bcthlem5  22294  bcth3  22297  ovolfcl  22417  ovolfioo  22418  ovolficc  22419  ovolficcss  22420  ovolfsval  22421  ovolmge0  22428  ovollb2lem  22439  ovolunlem1a  22447  ovoliunlem1  22453  ovoliunlem2  22454  ovoliun  22456  ovolicc1  22467  ovolicc2lem3  22470  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  voliunlem1  22501  volsup  22507  ioombl1lem2  22510  ovolfs2  22521  uniioovol  22534  uniiccvol  22535  uniioombllem3a  22540  uniioombllem3  22541  uniioombllem4  22542  uniioombllem5  22543  uniioombllem6  22544  dyadmbl  22556  volcn  22562  ismbf  22584  mbfadd  22615  mbfsub  22616  mbflimsup  22621  mbflimsupOLD  22622  0plef  22628  itg1climres  22670  mbfi1fseqlem1  22671  mbfi1fseqlem3  22673  mbfi1fseqlem4  22674  mbfi1fseqlem5  22675  mbfmul  22682  xrge0f  22687  itg2ge0  22691  itg2seq  22698  itg2uba  22699  itg2lea  22700  itg2eqa  22701  itg2splitlem  22704  itg2split  22705  itg2i1fseqle  22710  itg2i1fseq  22711  itg2i1fseq2  22712  itg2addlem  22714  bddmulibl  22794  ellimc3  22832  dvaddbr  22890  dvcobr  22898  dvcj  22902  dvfre  22903  dvcnvlem  22926  dvlip  22943  dvlipcn  22944  c1lip1  22947  tdeglem4  23007  tdeglem2  23008  coe1mul3  23046  ply1rem  23112  fta1g  23116  ig1pdvds  23126  ig1pdvdsOLD  23132  plyf  23150  plyeq0lem  23162  plypf1  23164  plyaddlem  23167  plymullem  23168  plyco  23193  dgreq  23196  0dgrb  23198  coefv0  23200  coeaddlem  23201  coemullem  23202  coemulc  23207  plycn  23213  dgrcolem2  23226  plycjlem  23228  plycj  23229  plyrecj  23231  plyreres  23234  dvply1  23235  vieta1lem2  23262  vieta1  23263  elqaalem2  23271  elqaalem2OLD  23274  aareccl  23280  aalioulem1  23286  ulmcaulem  23347  ulmcau  23348  ulmcn  23352  mtest  23357  psergf  23365  dvradcnv  23374  psercn2  23376  pserdvlem2  23381  pserdv2  23383  abelthlem6  23389  abelthlem8  23392  abelthlem9  23393  logtayl  23603  amgm  23914  ftalem1  23995  ftalem2  23996  ftalem3  23997  ftalem4  23998  ftalem5  23999  ftalem4OLD  24000  ftalem5OLD  24001  basellem2  24006  muinv  24120  dchrmulcl  24175  dchrinvcl  24179  dchrfi  24181  dchrghm  24182  dchrsum2  24194  dchrsum  24195  bposlem5  24214  lgscllem  24229  lgsval4a  24244  lgsneg  24245  lgsdir  24256  lgsdilem2  24257  lgsdi  24258  lgsne0  24259  lgseisenlem3  24277  rpvmasumlem  24323  dchrmusum2  24330  dchrvmasumiflem1  24337  dchrisum0ff  24343  dchrisum0flblem1  24344  dchrisum0fno1  24347  rpvmasum2  24348  dchrisum0re  24349  dchrisum0lem2a  24353  usgrarnedg  25109  usgraedg4  25112  usgrares1  25136  usgrwlknloop  25291  usgra2adedgwlkonALT  25342  usgra2wlkspthlem2  25346  cyclispthon  25359  fargshiftf  25362  usgrcyclnl2  25367  4cycl4dv  25393  el2wlkonotlem  25588  usg2wlkonot  25609  usg2wotspth  25610  vdgrnn0pnf  25635  frgrancvvdeqlemB  25764  ghgrplem2OLD  26093  lnoadd  26397  lnosub  26398  nmosetre  26403  nmooge0  26406  nmoub3i  26412  nmounbi  26415  phoeqi  26497  ubthlem1  26510  h2hcau  26630  h2hlm  26631  hoscl  27396  homcl  27397  hodcl  27398  hoaddcl  27409  homulcl  27410  homulid2  27451  homco1  27452  homulass  27453  hoadddi  27454  hoadddir  27455  hoeq1  27481  hoeq2  27482  adjsym  27484  nmopsetretALT  27514  nmfnsetre  27528  cnvadj  27543  hhcno  27555  hhcnf  27556  nmopub2tALT  27560  nmopge0  27562  unopf1o  27567  unoplin  27571  counop  27572  nmfnleub2  27577  nmfnge0  27578  hmoplin  27593  eigvalcl  27612  lnop0  27617  hmops  27671  hmopm  27672  nlelchi  27712  leop2  27775  leopadd  27783  leopmuli  27784  leopnmid  27789  hmopidmchi  27802  pjinvari  27842  sticl  27866  fcomptf  28262  rge0scvg  28763  esumcst  28892  esumfzf  28898  esumfsup  28899  esumfsupre  28900  hasheuni  28914  measdivcstOLD  29054  eulerpartlems  29201  eulerpartlemgc  29203  eulerpartlemb  29209  derangsn  29901  subfacp1lem5  29915  subfacp1lem6  29916  pconcon  29962  sconpi1  29970  txsconlem  29971  cvxscon  29974  cvmliftphtlem  30048  cvmlift3lem2  30051  cvmlift3lem4  30053  cvmlift3lem6  30055  elmrsubrn  30166  msubff  30176  msubvrs  30206  mclsssvlem  30208  ghomgrpilem2  30312  ghomcl  30318  ghomgsg  30319  faclim  30389  fprb  30420  soseq  30499  ptrecube  31904  heicant  31939  mblfinlem2  31942  itg2addnclem  31957  ftc1anclem1  31981  ftc1anclem2  31982  ftc1anclem4  31984  upixp  32020  fdc  32038  seqpo  32040  incsequz  32041  incsequz2  32042  metf1o  32048  geomcau  32052  sstotbnd2  32070  prdsbnd  32089  ismtyima  32099  ismtyhmeolem  32100  heiborlem3  32109  heiborlem6  32112  heiborlem10  32116  bfplem1  32118  ghomco  32145  mzpclall  35538  mzprename  35560  rexrabdioph  35606  rmydioph  35839  rmxdioph  35841  expdiophlem2  35847  expdioph  35848  pw2f1ocnv  35862  kelac1  35891  rngunsnply  36009  ofsubid  36643  ofdivrec  36645  ofdivcan4  36646  ofdivdiv2  36647  dvconstbi  36653  refsum2cnlem1  37331  dffo3f  37411  climinf  37624  climinfOLD  37625  stoweidlem26  37826  stoweidlem60  37861  stoweid  37865  caratheodory  38257  elhoi  38268  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  2f1fvneq  38877  usgra2pthlem1  39286  mgmhmpropd  39404  rmsupp0  39774  domnmsuppn0  39775  gsumlsscl  39789  lincfsuppcl  39827  linccl  39828  lincdifsn  39838  lincsum  39843  lincscm  39844  lincscmcl  39846  lincext1  39868  lindslinindimp2lem1  39872  lindslinindimp2lem4  39875  lindslinindsimp2lem5  39876  snlindsntor  39885  lincresunitlem2  39890  lincresunit3lem1  39893  lincresunit3lem2  39894  lincresunit3  39895  lincreslvec3  39896  isldepslvec2  39899  zlmodzxzldeplem3  39916  aacllem  40161
  Copyright terms: Public domain W3C validator