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

Theorem ffvelrn 5940
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 5657 . . 3  |-  ( F : A --> B  ->  F  Fn  A )
2 fnfvelrn 5939 . . 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 5663 . . . 4  |-  ( F : A --> B  ->  ran  F  C_  B )
54sseld 3453 . . 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 1758   ran crn 4939    Fn wfn 5511   -->wf 5512   ` cfv 5516
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-fv 5524
This theorem is referenced by:  ffvelrni  5941  ffvelrnda  5942  dffo3  5957  foco2  5962  ffnfv  5968  ffvresb  5973  fcompt  5978  fsn2  5982  fvconst  5996  fcofo  6091  cocan1  6094  isocnv  6120  isocnv3  6122  isores2  6123  isopolem  6135  isosolem  6137  fovrn  6333  off  6434  fnwelem  6787  smofvon2  6917  smorndom  6929  omsmolem  7192  omsmo  7193  mapsncnv  7359  2dom  7482  xpdom2  7506  domunsncan  7511  xpmapenlem  7578  fiint  7689  ordiso2  7830  infdifsn  7963  cantnflem1  7998  cantnflem1OLD  8021  wemapwe  8029  wemapweOLD  8030  cnfcom3lem  8037  cnfcom3lemOLD  8045  fseqenlem1  8295  finacn  8321  ackbij1lem12  8501  cofsmo  8539  cfsmolem  8540  cfcoflem  8542  coftr  8543  isf32lem6  8628  isf32lem7  8629  isf34lem7  8649  isf34lem6  8650  acncc  8710  axdc2lem  8718  axdc3lem2  8721  axdc3lem4  8723  axdc4lem  8725  axcclem  8727  ttukeylem6  8784  alephreg  8847  pwcfsdom  8848  canthp1lem2  8921  canthp1  8922  pwfseqlem1  8926  pwfseqlem4a  8929  gruf  9079  fsequb2  11899  axdc4uzlem  11905  seqf1o  11948  hashf1lem1  12310  eqs1  12402  shftf  12670  limsupgre  13061  rlimuni  13130  lo1resb  13144  o1resb  13146  o1of2  13192  o1rlimmul  13198  isercolllem1  13244  isercolllem2  13245  isercolllem3  13246  isercoll  13247  climsup  13249  iseralt  13264  sumeq2ii  13272  summolem2a  13294  isumcl  13330  isumshft  13404  climcndslem2  13415  climcnds  13416  mertenslem2  13447  rpnnen2lem10  13608  ruclem8  13621  ruclem12  13625  3dvds  13698  smueqlem  13788  nn0seqcvgd  13847  algrf  13850  eucalg  13864  phimullem  13956  pcmpt  14056  pcprod  14059  vdwlem11  14154  vdwnnlem3  14160  ramlb  14182  0ram  14183  ramcl  14192  imasaddfnlem  14568  imasaddflem  14570  mhmpropd  15572  ghmsub  15857  cntzmhm  15958  f1omvdconj  16054  pj1ghm  16304  gsumzaddlem  16512  gsumzadd  16513  gsumzaddlemOLD  16514  gsumzaddOLD  16515  dprdfadd  16615  dprdfaddOLD  16622  dprdf1o  16634  subgdmdprd  16636  gsumdixpOLD  16806  gsumdixp  16807  lspcl  17163  psrbaglesupp  17541  psrbaglesuppOLD  17542  psrbaglefi  17547  psrbaglefiOLD  17548  resspsrmul  17596  evlslem4OLD  17697  evlslem4  17698  evlslem3  17707  fvcoe1  17770  psropprmul  17800  00ply1bas  17802  subrgvr1cl  17823  coe1mul2lem1  17828  coe1tmmul  17838  ply1coe  17855  ply1coeOLD  17856  evl1val  17872  evl1sca  17877  pf1const  17889  znunit  18105  frlmsslsp  18332  frlmsslspOLD  18333  frlmup2  18336  lindfmm  18365  islindf4  18376  1mavmul  18470  mavmulass  18471  marepvcl  18491  1marepvmarrepid  18497  cramerimplem1  18605  hauscmplem  19125  ptbasid  19264  ptpjcn  19300  upxp  19312  uptx  19314  txcmplem2  19331  xkopt  19344  txhmeo  19492  alexsubALTlem3  19737  nrginvrcn  20388  nmoi  20423  nmoleub  20426  cncfmet  20600  cnheibor  20643  evth  20647  pcopt  20710  pcopt2  20711  pcorevlem  20714  pi1xfrf  20741  pi1xfr  20743  pi1xfrcnvlem  20744  iscauf  20907  iscmet3lem1  20918  iscmet3lem2  20919  iscmet3  20920  causs  20925  bcthlem5  20955  bcth3  20958  ovolfcl  21066  ovolfioo  21067  ovolficc  21068  ovolficcss  21069  ovolfsval  21070  ovolmge0  21076  ovollb2lem  21087  ovolunlem1a  21095  ovoliunlem1  21101  ovoliunlem2  21102  ovoliun  21104  ovolicc1  21115  ovolicc2lem3  21118  ovolicc2lem4  21119  ovolicc2lem5  21120  voliunlem1  21147  volsup  21153  ioombl1lem2  21156  ovolfs2  21167  uniioovol  21175  uniiccvol  21176  uniioombllem3a  21180  uniioombllem3  21181  uniioombllem4  21182  uniioombllem5  21183  uniioombllem6  21184  dyadmbl  21196  volcn  21202  ismbf  21224  mbfadd  21255  mbfsub  21256  mbflimsup  21260  0plef  21266  itg1climres  21308  mbfi1fseqlem1  21309  mbfi1fseqlem3  21311  mbfi1fseqlem4  21312  mbfi1fseqlem5  21313  mbfmul  21320  xrge0f  21325  itg2ge0  21329  itg2seq  21336  itg2uba  21337  itg2lea  21338  itg2eqa  21339  itg2splitlem  21342  itg2split  21343  itg2i1fseqle  21348  itg2i1fseq  21349  itg2i1fseq2  21350  itg2addlem  21352  bddmulibl  21432  ellimc3  21470  dvaddbr  21528  dvcobr  21536  dvcj  21540  dvfre  21541  dvcnvlem  21564  dvlip  21581  dvlipcn  21582  c1lip1  21585  tdeglem4  21645  tdeglem2  21646  coe1mul3  21687  ply1rem  21751  fta1g  21755  ig1pdvds  21764  plyf  21782  plyeq0lem  21794  plypf1  21796  plyaddlem  21799  plymullem  21800  plyco  21825  dgreq  21828  0dgrb  21830  coefv0  21831  coeaddlem  21832  coemullem  21833  coemulc  21838  plycn  21844  dgrcolem2  21857  plycjlem  21859  plycj  21860  plyrecj  21862  plyreres  21865  dvply1  21866  vieta1lem2  21893  vieta1  21894  elqaalem2  21902  aareccl  21908  aalioulem1  21914  ulmcaulem  21975  ulmcau  21976  ulmcn  21980  mtest  21985  psergf  21993  dvradcnv  22002  psercn2  22004  pserdvlem2  22009  pserdv2  22011  abelthlem6  22017  abelthlem8  22020  abelthlem9  22021  logtayl  22221  amgm  22500  ftalem1  22526  ftalem2  22527  ftalem3  22528  ftalem4  22529  ftalem5  22530  basellem2  22535  muinv  22649  dchrmulcl  22704  dchrinvcl  22708  dchrfi  22710  dchrghm  22711  dchrsum2  22723  dchrsum  22724  bposlem5  22743  lgscllem  22758  lgsval4a  22773  lgsneg  22774  lgsdir  22785  lgsdilem2  22786  lgsdi  22787  lgsne0  22788  lgseisenlem3  22806  rpvmasumlem  22852  dchrmusum2  22859  dchrvmasumiflem1  22866  dchrisum0ff  22872  dchrisum0flblem1  22873  dchrisum0fno1  22876  rpvmasum2  22877  dchrisum0re  22878  dchrisum0lem2a  22882  usgrarnedg  23438  usgraedg4  23440  usgrares1  23458  usgrnloop  23597  cyclispthon  23654  fargshiftf  23657  usgrcyclnl2  23662  4cycl4dv  23688  vdgrnn0pnf  23714  ghgrplem2  23989  lnoadd  24293  lnosub  24294  nmosetre  24299  nmooge0  24302  nmoub3i  24308  nmounbi  24311  phoeqi  24393  ubthlem1  24406  h2hcau  24516  h2hlm  24517  hoscl  25284  homcl  25285  hodcl  25286  hoaddcl  25297  homulcl  25298  homulid2  25339  homco1  25340  homulass  25341  hoadddi  25342  hoadddir  25343  hoeq1  25369  hoeq2  25370  adjsym  25372  nmopsetretALT  25402  nmfnsetre  25416  cnvadj  25431  hhcno  25443  hhcnf  25444  nmopub2tALT  25448  nmopge0  25450  unopf1o  25455  unoplin  25459  counop  25460  nmfnleub2  25465  nmfnge0  25466  hmoplin  25481  eigvalcl  25500  lnop0  25505  hmops  25559  hmopm  25560  nlelchi  25600  leop2  25663  leopadd  25671  leopmuli  25672  leopnmid  25677  hmopidmchi  25690  pjinvari  25730  sticl  25754  fcomptf  26114  rge0scvg  26513  esumcst  26648  esumfzf  26652  esumfsup  26653  esumfsupre  26654  hasheuni  26668  measdivcstOLD  26772  eulerpartlems  26877  eulerpartlemgc  26879  eulerpartlemb  26885  derangsn  27192  subfacp1lem5  27206  subfacp1lem6  27207  pconcon  27254  sconpi1  27262  txsconlem  27263  cvxscon  27266  cvmliftphtlem  27340  cvmlift3lem2  27343  cvmlift3lem4  27345  cvmlift3lem6  27347  ghomgrpilem2  27439  ghomcl  27445  ghomgsg  27446  prodeq2ii  27560  prodmolem2a  27581  iprodcl  27635  faclim  27686  fprb  27718  soseq  27849  heicant  28564  mblfinlem2  28567  itg2addnclem  28581  ftc1anclem1  28605  ftc1anclem2  28606  ftc1anclem4  28608  upixp  28761  fdc  28779  seqpo  28781  incsequz  28782  incsequz2  28783  metf1o  28789  geomcau  28793  sstotbnd2  28811  prdsbnd  28830  ismtyima  28840  ismtyhmeolem  28841  heiborlem3  28850  heiborlem6  28853  heiborlem10  28857  bfplem1  28859  ghomco  28886  mzpclall  29201  mzprename  29224  rexrabdioph  29270  rmydioph  29501  rmxdioph  29503  expdiophlem2  29509  expdioph  29510  pw2f1ocnv  29524  kelac1  29554  rngunsnply  29668  ofsubid  29736  ofdivrec  29738  ofdivcan4  29739  ofdivdiv2  29740  dvconstbi  29746  refsum2cnlem1  29897  climinf  29917  stoweidlem26  29959  stoweidlem60  29993  stoweid  29996  2f1fvneq  30281  wwlktovf  30389  usgra2wlkspthlem2  30435  usgra2pthlem1  30438  el2wlkonotlem  30519  usg2wlkonot  30540  usg2wotspth  30541  frgrancvvdeqlemB  30769  rmsupp0  30919  domnmsuppn0  30920  gsummptnn0fzfv  30949  gsumlsscl  30958  lincfsuppcl  31054  linccl  31055  lincdifsn  31065  lincsum  31070  lincscm  31071  lincscmcl  31073  lincext1  31095  lindslinindimp2lem1  31099  lindslinindimp2lem4  31102  lindslinindsimp2lem5  31103  snlindsntor  31112  lincresunitlem2  31117  lincresunit3lem1  31120  lincresunit3lem2  31121  lincresunit3  31122  lincreslvec3  31123  isldepslvec2  31126  zlmodzxzldeplem3  31151  pmatcollpw4fi1lem1  31242  pmatcollpw4fi1lem2  31243  cpmadugsumlemF  31330  cpmadugsumfi  31331  cayleyhamilton1  31347
  Copyright terms: Public domain W3C validator