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 3469 . . 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 1870   ran crn 4855    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 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-rab 2791  df-v 3089  df-sbc 3306  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-id 4769  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  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  7083  smorndom  7095  omsmolem  7362  omsmo  7363  mapsncnv  7526  2dom  7649  xpdom2  7673  domunsncan  7678  xpmapenlem  7745  fiint  7854  ordiso2  8030  infdifsn  8161  cantnflem1  8193  wemapwe  8201  cnfcom3lem  8207  fseqenlem1  8453  finacn  8479  ackbij1lem12  8659  cofsmo  8697  cfsmolem  8698  cfcoflem  8700  coftr  8701  isf32lem6  8786  isf32lem7  8787  isf34lem7  8807  isf34lem6  8808  acncc  8868  axdc2lem  8876  axdc3lem2  8879  axdc3lem4  8881  axdc4lem  8883  axcclem  8885  ttukeylem6  8942  alephreg  9005  pwcfsdom  9006  canthp1lem2  9077  canthp1  9078  pwfseqlem1  9082  pwfseqlem4a  9085  gruf  9235  fsequb2  12186  axdc4uzlem  12192  seqf1o  12251  hashf1lem1  12613  wwlktovf  13010  shftf  13121  limsupgre  13520  limsupgreOLD  13521  rlimuni  13592  lo1resb  13606  o1resb  13608  o1of2  13654  o1rlimmul  13660  isercolllem1  13706  isercolllem2  13707  isercolllem3  13708  isercoll  13709  climsup  13711  iseralt  13729  sumeq2ii  13737  summolem2a  13759  isumcl  13800  isumshft  13875  climcndslem2  13886  climcnds  13887  mertenslem2  13919  prodeq2ii  13945  prodmolem2a  13966  iprodcl  14032  rpnnen2lem10  14254  ruclem8  14267  ruclem12  14271  3dvds  14347  smueqlem  14438  nn0seqcvgd  14500  algrf  14503  eucalg  14517  phimullem  14687  pcmpt  14791  pcprod  14794  vdwlem11  14895  vdwnnlem3  14901  ramlb  14931  0ram  14932  ramcl  14941  prmgaplcmlem1OLD  14966  prmgaplcmlem2OLD  14967  prmdvdsprmorpOLD  14970  prmgapprmorlemOLD  14971  prmorlelcmfOLD  14974  prmorlelcmsOLDOLD  14976  prmgaplem8  14982  imasaddfnlem  15376  imasaddflem  15378  mhmpropd  16530  ghmsub  16833  cntzmhm  16934  f1omvdconj  17029  pj1ghm  17279  gsumzaddlem  17480  gsumzadd  17481  gsummptnn0fzfv  17543  dprdfadd  17579  subgdmdprd  17593  gsumdixp  17763  lspcl  18125  psrbaglesupp  18518  psrbaglefi  18522  resspsrmul  18567  evlslem4  18657  evlslem3  18663  fvcoe1  18726  psropprmul  18757  00ply1bas  18759  subrgvr1cl  18781  coe1mul2lem1  18786  coe1tmmul  18796  ply1coe  18815  ply1coeOLD  18816  evl1val  18843  evl1sca  18848  pf1const  18860  znunit  19056  frlmsslsp  19276  frlmup2  19279  lindfmm  19307  islindf4  19318  1mavmul  19495  mavmulass  19496  marepvcl  19516  1marepvmarrepid  19522  cramerimplem1  19630  pmatcollpw3fi1lem1  19732  pmatcollpw3fi1lem2  19733  cpmadugsumlemF  19822  cpmadugsumfi  19823  cayleyhamilton1  19838  hauscmplem  20343  ptbasid  20512  ptpjcn  20548  upxp  20560  uptx  20562  txcmplem2  20579  xkopt  20592  txhmeo  20740  alexsubALTlem3  20986  nrginvrcn  21616  nmoi  21651  nmoleub  21654  cncfmet  21827  cnheibor  21870  evth  21874  pcopt  21937  pcopt2  21938  pcorevlem  21941  pi1xfrf  21968  pi1xfr  21970  pi1xfrcnvlem  21971  iscauf  22134  iscmet3lem1  22145  iscmet3lem2  22146  iscmet3  22147  causs  22152  bcthlem5  22180  bcth3  22183  ovolfcl  22289  ovolfioo  22290  ovolficc  22291  ovolficcss  22292  ovolfsval  22293  ovolmge0  22299  ovollb2lem  22310  ovolunlem1a  22318  ovoliunlem1  22324  ovoliunlem2  22325  ovoliun  22327  ovolicc1  22338  ovolicc2lem3  22341  ovolicc2lem4  22342  ovolicc2lem5  22343  voliunlem1  22371  volsup  22377  ioombl1lem2  22380  ovolfs2  22391  uniioovol  22404  uniiccvol  22405  uniioombllem3a  22410  uniioombllem3  22411  uniioombllem4  22412  uniioombllem5  22413  uniioombllem6  22414  dyadmbl  22426  volcn  22432  ismbf  22454  mbfadd  22485  mbfsub  22486  mbflimsup  22491  mbflimsupOLD  22492  0plef  22498  itg1climres  22540  mbfi1fseqlem1  22541  mbfi1fseqlem3  22543  mbfi1fseqlem4  22544  mbfi1fseqlem5  22545  mbfmul  22552  xrge0f  22557  itg2ge0  22561  itg2seq  22568  itg2uba  22569  itg2lea  22570  itg2eqa  22571  itg2splitlem  22574  itg2split  22575  itg2i1fseqle  22580  itg2i1fseq  22581  itg2i1fseq2  22582  itg2addlem  22584  bddmulibl  22664  ellimc3  22702  dvaddbr  22760  dvcobr  22768  dvcj  22772  dvfre  22773  dvcnvlem  22796  dvlip  22813  dvlipcn  22814  c1lip1  22817  tdeglem4  22877  tdeglem2  22878  coe1mul3  22916  ply1rem  22980  fta1g  22984  ig1pdvds  22993  plyf  23011  plyeq0lem  23023  plypf1  23025  plyaddlem  23028  plymullem  23029  plyco  23054  dgreq  23057  0dgrb  23059  coefv0  23061  coeaddlem  23062  coemullem  23063  coemulc  23068  plycn  23074  dgrcolem2  23087  plycjlem  23089  plycj  23090  plyrecj  23092  plyreres  23095  dvply1  23096  vieta1lem2  23123  vieta1  23124  elqaalem2  23132  aareccl  23138  aalioulem1  23144  ulmcaulem  23205  ulmcau  23206  ulmcn  23210  mtest  23215  psergf  23223  dvradcnv  23232  psercn2  23234  pserdvlem2  23239  pserdv2  23241  abelthlem6  23247  abelthlem8  23250  abelthlem9  23251  logtayl  23461  amgm  23772  ftalem1  23853  ftalem2  23854  ftalem3  23855  ftalem4  23856  ftalem5  23857  basellem2  23862  muinv  23976  dchrmulcl  24031  dchrinvcl  24035  dchrfi  24037  dchrghm  24038  dchrsum2  24050  dchrsum  24051  bposlem5  24070  lgscllem  24085  lgsval4a  24100  lgsneg  24101  lgsdir  24112  lgsdilem2  24113  lgsdi  24114  lgsne0  24115  lgseisenlem3  24133  rpvmasumlem  24179  dchrmusum2  24186  dchrvmasumiflem1  24193  dchrisum0ff  24199  dchrisum0flblem1  24200  dchrisum0fno1  24203  rpvmasum2  24204  dchrisum0re  24205  dchrisum0lem2a  24209  usgrarnedg  24948  usgraedg4  24951  usgrares1  24974  usgrnloop  25129  usgra2adedgwlkonALT  25180  usgra2wlkspthlem2  25184  cyclispthon  25197  fargshiftf  25200  usgrcyclnl2  25205  4cycl4dv  25231  el2wlkonotlem  25426  usg2wlkonot  25447  usg2wotspth  25448  vdgrnn0pnf  25473  frgrancvvdeqlemB  25602  ghgrplem2OLD  25931  lnoadd  26235  lnosub  26236  nmosetre  26241  nmooge0  26244  nmoub3i  26250  nmounbi  26253  phoeqi  26335  ubthlem1  26348  h2hcau  26458  h2hlm  26459  hoscl  27224  homcl  27225  hodcl  27226  hoaddcl  27237  homulcl  27238  homulid2  27279  homco1  27280  homulass  27281  hoadddi  27282  hoadddir  27283  hoeq1  27309  hoeq2  27310  adjsym  27312  nmopsetretALT  27342  nmfnsetre  27356  cnvadj  27371  hhcno  27383  hhcnf  27384  nmopub2tALT  27388  nmopge0  27390  unopf1o  27395  unoplin  27399  counop  27400  nmfnleub2  27405  nmfnge0  27406  hmoplin  27421  eigvalcl  27440  lnop0  27445  hmops  27499  hmopm  27500  nlelchi  27540  leop2  27603  leopadd  27611  leopmuli  27612  leopnmid  27617  hmopidmchi  27630  pjinvari  27670  sticl  27694  fcomptf  28091  rge0scvg  28585  esumcst  28714  esumfzf  28720  esumfsup  28721  esumfsupre  28722  hasheuni  28736  measdivcstOLD  28876  eulerpartlems  29010  eulerpartlemgc  29012  eulerpartlemb  29018  derangsn  29672  subfacp1lem5  29686  subfacp1lem6  29687  pconcon  29733  sconpi1  29741  txsconlem  29742  cvxscon  29745  cvmliftphtlem  29819  cvmlift3lem2  29822  cvmlift3lem4  29824  cvmlift3lem6  29826  elmrsubrn  29937  msubff  29947  msubvrs  29977  mclsssvlem  29979  ghomgrpilem2  30083  ghomcl  30089  ghomgsg  30090  faclim  30160  fprb  30191  soseq  30270  ptrecube  31634  heicant  31669  mblfinlem2  31672  itg2addnclem  31687  ftc1anclem1  31711  ftc1anclem2  31712  ftc1anclem4  31714  upixp  31750  fdc  31768  seqpo  31770  incsequz  31771  incsequz2  31772  metf1o  31778  geomcau  31782  sstotbnd2  31800  prdsbnd  31819  ismtyima  31829  ismtyhmeolem  31830  heiborlem3  31839  heiborlem6  31842  heiborlem10  31846  bfplem1  31848  ghomco  31875  mzpclall  35268  mzprename  35290  rexrabdioph  35336  rmydioph  35565  rmxdioph  35567  expdiophlem2  35573  expdioph  35574  pw2f1ocnv  35588  kelac1  35617  rngunsnply  35728  ofsubid  36300  ofdivrec  36302  ofdivcan4  36303  ofdivdiv2  36304  dvconstbi  36310  refsum2cnlem1  36988  dffo3f  37063  climinf  37246  climinfOLD  37247  stoweidlem26  37445  stoweidlem60  37480  stoweid  37484  caratheodory  37848  nnsum4primeseven  38275  nnsum4primesevenALTV  38276  2f1fvneq  38374  usgra2pthlem1  38413  mgmhmpropd  38533  rmsupp0  38903  domnmsuppn0  38904  gsumlsscl  38918  lincfsuppcl  38956  linccl  38957  lincdifsn  38967  lincsum  38972  lincscm  38973  lincscmcl  38975  lincext1  38997  lindslinindimp2lem1  39001  lindslinindimp2lem4  39004  lindslinindsimp2lem5  39005  snlindsntor  39014  lincresunitlem2  39019  lincresunit3lem1  39022  lincresunit3lem2  39023  lincresunit3  39024  lincreslvec3  39025  isldepslvec2  39028  zlmodzxzldeplem3  39045  aacllem  39291
  Copyright terms: Public domain W3C validator