Theorem ffvelrn 6357

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

Step	Hyp	Ref	Expression
1		ffn 6045	. . 3 |- ( F : A --> B -> F Fn A )
2		fnfvelrn 6356	. . 3 |- ( ( F Fn A /\ C e. A ) -> ( F ` C ) e. ran F )
3	1, 2	sylan 488	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. ran F )
4		frn 6053	. . . 4 |- ( F : A --> B -> ran F C_ B )
5	4	sseld 3602	. . 3 |- ( F : A --> B -> ( ( F ` C ) e. ran F -> ( F ` C ) e. B ) )
6	5	adantr 481	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( ( F ` C ) e. ran F -> ( F ` C ) e. B ) )
7	3, 6	mpd 15	1 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   ran crn 5115   Fn wfn 5883   -->wf 5884   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  ffvelrni  6358  ffvelrnda  6359  dffo3  6374  foco2  6379  foco2OLD  6380  ffnfv  6388  ffvresb  6394  fcompt  6400  fsn2  6403  fvconst  6431  f1cofveqaeq  6515  2f1fvneq  6517  fcofo  6543  cocan1  6546  isocnv  6580  isocnv3  6582  isores2  6583  isopolem  6595  isosolem  6597  fovrn  6804  off  6912  fnwelem  7292  smofvon2  7453  smorndom  7465  omsmolem  7733  omsmo  7734  mapsncnv  7904  2dom  8029  xpdom2  8055  domunsncan  8060  xpmapenlem  8127  fiint  8237  ordiso2  8420  infdifsn  8554  cantnflem1  8586  wemapwe  8594  cnfcom3lem  8600  fseqenlem1  8847  finacn  8873  ackbij1lem12  9053  cofsmo  9091  cfsmolem  9092  cfcoflem  9094  coftr  9095  isf32lem6  9180  isf32lem7  9181  isf34lem7  9201  isf34lem6  9202  acncc  9262  axdc2lem  9270  axdc3lem2  9273  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  ttukeylem6  9336  alephreg  9404  pwcfsdom  9405  canthp1lem2  9475  canthp1  9476  pwfseqlem1  9480  pwfseqlem4a  9483  gruf  9633  fsequb2  12775  axdc4uzlem  12782  seqf1o  12842  hashf1lem1  13239  wwlktovf  13699  shftf  13819  limsupgre  14212  rlimuni  14281  lo1resb  14295  o1resb  14297  o1of2  14343  o1rlimmul  14349  isercolllem1  14395  isercolllem2  14396  isercolllem3  14397  isercoll  14398  climsup  14400  iseralt  14415  sumeq2ii  14423  summolem2a  14446  isumcl  14492  isumshft  14571  climcndslem2  14582  climcnds  14583  mertenslem2  14617  prodeq2ii  14643  prodmolem2a  14664  iprodcl  14732  rpnnen2lem10  14952  ruclem8  14966  ruclem12  14970  3dvds  15052  3dvdsOLD  15053  smueqlem  15212  nn0seqcvgd  15283  algrf  15286  eucalg  15300  phimullem  15484  pcmpt  15596  pcprod  15599  vdwlem11  15695  vdwnnlem3  15701  ramlb  15723  0ram  15724  ramcl  15733  prmgaplem8  15762  imasaddfnlem  16188  imasaddflem  16190  mhmpropd  17341  ghmsub  17668  cntzmhm  17771  f1omvdconj  17866  pj1ghm  18116  gsumzaddlem  18321  gsumzadd  18322  gsummptnn0fzfv  18384  dprdfadd  18419  subgdmdprd  18433  gsumdixp  18609  lspcl  18976  psrbaglesupp  19368  psrbaglefi  19372  resspsrmul  19417  evlslem4  19508  evlslem3  19514  fvcoe1  19577  psropprmul  19608  00ply1bas  19610  subrgvr1cl  19632  coe1mul2lem1  19637  coe1tmmul  19647  ply1coe  19666  evl1val  19693  evl1sca  19698  pf1const  19710  znunit  19912  frlmsslsp  20135  frlmup2  20138  lindfmm  20166  islindf4  20177  1mavmul  20354  mavmulass  20355  marepvcl  20375  1marepvmarrepid  20381  cramerimplem1  20489  pmatcollpw3fi1lem1  20591  pmatcollpw3fi1lem2  20592  cpmadugsumlemF  20681  cpmadugsumfi  20682  cayleyhamilton1  20697  hauscmplem  21209  ptbasid  21378  ptpjcn  21414  upxp  21426  uptx  21428  txcmplem2  21445  xkopt  21458  txhmeo  21606  alexsubALTlem3  21853  nrginvrcn  22496  nmoi  22532  nmoleub  22535  cncfmet  22711  cnheibor  22754  evth  22758  pcopt  22822  pcopt2  22823  pcorevlem  22826  pi1xfrf  22853  pi1xfr  22855  pi1xfrcnvlem  22856  iscauf  23078  iscmet3lem1  23089  iscmet3lem2  23090  iscmet3  23091  causs  23096  bcthlem5  23125  bcth3  23128  ovolfcl  23235  ovolfioo  23236  ovolficc  23237  ovolficcss  23238  ovolfsval  23239  ovolmge0  23245  ovollb2lem  23256  ovolunlem1a  23264  ovoliunlem1  23270  ovoliunlem2  23271  ovoliun  23273  ovolicc1  23284  ovolicc2lem3  23287  ovolicc2lem4  23288  ovolicc2lem5  23289  voliunlem1  23318  volsup  23324  ioombl1lem2  23327  ovolfs2  23339  uniioovol  23347  uniiccvol  23348  uniioombllem3a  23352  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  uniioombllem6  23356  dyadmbl  23368  volcn  23374  ismbf  23397  mbfadd  23428  mbfsub  23429  mbflimsup  23433  0plef  23439  itg1climres  23481  mbfi1fseqlem1  23482  mbfi1fseqlem3  23484  mbfi1fseqlem4  23485  mbfi1fseqlem5  23486  mbfmul  23493  xrge0f  23498  itg2ge0  23502  itg2seq  23509  itg2uba  23510  itg2lea  23511  itg2eqa  23512  itg2splitlem  23515  itg2split  23516  itg2i1fseqle  23521  itg2i1fseq  23522  itg2i1fseq2  23523  itg2addlem  23525  bddmulibl  23605  ellimc3  23643  dvaddbr  23701  dvcobr  23709  dvcj  23713  dvfre  23714  dvcnvlem  23739  dvlip  23756  dvlipcn  23757  c1lip1  23760  tdeglem4  23820  tdeglem2  23821  coe1mul3  23859  ply1rem  23923  fta1g  23927  ig1pdvds  23936  plyf  23954  plyeq0lem  23966  plypf1  23968  plyaddlem  23971  plymullem  23972  plyco  23997  dgreq  24000  0dgrb  24002  coefv0  24004  coeaddlem  24005  coemullem  24006  coemulc  24011  plycn  24017  dgrcolem2  24030  plycjlem  24032  plycj  24033  plyrecj  24035  plyreres  24038  dvply1  24039  vieta1lem2  24066  vieta1  24067  elqaalem2  24075  aareccl  24081  aalioulem1  24087  ulmcaulem  24148  ulmcau  24149  ulmcn  24153  mtest  24158  psergf  24166  dvradcnv  24175  psercn2  24177  pserdvlem2  24182  pserdv2  24184  abelthlem6  24190  abelthlem8  24193  abelthlem9  24194  logtayl  24406  amgm  24717  ftalem1  24799  ftalem2  24800  ftalem3  24801  ftalem4  24802  ftalem5  24803  basellem2  24808  muinv  24919  dchrmulcl  24974  dchrinvcl  24978  dchrfi  24980  dchrghm  24981  dchrsum2  24993  dchrsum  24994  bposlem5  25013  lgscllem  25029  lgsval4a  25044  lgsneg  25046  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  lgseisenlem3  25102  rpvmasumlem  25176  dchrmusum2  25183  dchrvmasumiflem1  25190  dchrisum0ff  25196  dchrisum0flblem1  25197  dchrisum0fno1  25200  rpvmasum2  25201  dchrisum0re  25202  dchrisum0lem2a  25206  upgrreslem  26196  umgrreslem  26197  wlkpvtx  26555  wlkepvtx  26556  wlkres  26567  usgr2pthlem  26659  frgrncvvdeqlem8  27170  lnoadd  27613  lnosub  27614  nmosetre  27619  nmooge0  27622  nmoub3i  27628  nmounbi  27631  phoeqi  27713  ubthlem1  27726  h2hcau  27836  h2hlm  27837  hoscl  28604  homcl  28605  hodcl  28606  hoaddcl  28617  homulcl  28618  homulid2  28659  homco1  28660  homulass  28661  hoadddi  28662  hoadddir  28663  hoeq1  28689  hoeq2  28690  adjsym  28692  nmopsetretALT  28722  nmfnsetre  28736  cnvadj  28751  hhcno  28763  hhcnf  28764  nmopub2tALT  28768  nmopge0  28770  unopf1o  28775  unoplin  28779  counop  28780  nmfnleub2  28785  nmfnge0  28786  hmoplin  28801  eigvalcl  28820  lnop0  28825  hmops  28879  hmopm  28880  nlelchi  28920  leop2  28983  leopadd  28991  leopmuli  28992  leopnmid  28997  hmopidmchi  29010  pjinvari  29050  sticl  29074  fcomptf  29458  rge0scvg  29995  esumcst  30125  esumfzf  30131  esumfsup  30132  esumfsupre  30133  hasheuni  30147  measdivcstOLD  30287  eulerpartlems  30422  eulerpartlemgc  30424  eulerpartlemb  30430  derangsn  31152  subfacp1lem5  31166  subfacp1lem6  31167  pconnconn  31213  sconnpi1  31221  txsconnlem  31222  cvxsconn  31225  cvmliftphtlem  31299  cvmlift3lem2  31302  cvmlift3lem4  31304  cvmlift3lem6  31306  elmrsubrn  31417  msubff  31427  msubvrs  31457  mclsssvlem  31459  faclim  31632  fprb  31669  soseq  31751  curf  33387  uncf  33388  curunc  33391  unccur  33392  matunitlindflem1  33405  matunitlindflem2  33406  ptrecube  33409  heicant  33444  mblfinlem2  33447  itg2addnclem  33461  ftc1anclem1  33485  ftc1anclem2  33486  ftc1anclem4  33488  upixp  33524  fdc  33541  seqpo  33543  incsequz  33544  incsequz2  33545  metf1o  33551  geomcau  33555  sstotbnd2  33573  prdsbnd  33592  ismtyima  33602  ismtyhmeolem  33603  heiborlem3  33612  heiborlem6  33615  heiborlem10  33619  bfplem1  33621  ghomco  33690  mzpclall  37290  mzprename  37312  rexrabdioph  37358  rmydioph  37581  rmxdioph  37583  expdiophlem2  37589  expdioph  37590  pw2f1ocnv  37604  kelac1  37633  rngunsnply  37743  ofsubid  38523  ofdivrec  38525  ofdivcan4  38526  ofdivdiv2  38527  dvconstbi  38533  refsum2cnlem1  39196  dffo3f  39364  climinf  39838  stoweidlem26  40243  stoweidlem60  40277  stoweid  40280  dmvolsal  40564  caratheodory  40742  elhoi  40756  smfresal  40995  fargshiftf  41376  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  mgmhmpropd  41785  rmsupp0  42149  domnmsuppn0  42150  gsumlsscl  42164  lincfsuppcl  42202  linccl  42203  lincdifsn  42213  lincsum  42218  lincscm  42219  lincscmcl  42221  lincext1  42243  lindslinindimp2lem1  42247  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  snlindsntor  42260  lincresunitlem2  42265  lincresunit3lem1  42268  lincresunit3lem2  42269  lincresunit3  42270  lincreslvec3  42271  isldepslvec2  42274  zlmodzxzldeplem3  42291  aacllem  42547