Theorem ffvelcdm 7025

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)

Assertion

Ref	Expression
ffvelcdm	⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdm

Step	Hyp	Ref	Expression
1		ffn 6658	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7024	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 587	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6665	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3915	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 482	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2121  ran crn 5621   Fn wfn 6483  ⟶wf 6484  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-fv 6496

This theorem is referenced by:  ffvelcdmi  7027  ffvelcdmda  7028  dffo3  7046  dffo3f  7050  foco2  7053  ffnfv  7063  ffvresb  7070  fcompt  7078  fsn2  7081  fvconst  7109  fprb  7141  f1cofveqaeq  7204  fcofo  7235  cocan1  7238  fvf1pr  7254  isocnv  7277  isocnv3  7279  isores2  7280  isopolem  7292  isosolem  7294  fovcdm  7529  off  7641  fnwelem  8073  soseq  8101  smofvon2  8289  smocdmdom  8301  omsmolem  8587  omsmo  8588  fsetfcdm  8801  mapfvd  8821  mapsncnv  8835  2dom  8971  xpdom2  9004  domunsncan  9009  xpmapenlem  9076  fiint  9231  infdifsn  9573  cantnflem1  9605  wemapwe  9613  cnfcom3lem  9619  updjudhf  9850  fseqenlem1  9941  finacn  9967  ackbij1lem12  10147  cofsmo  10187  cfsmolem  10188  cfcoflem  10190  coftr  10191  isf32lem6  10276  isf32lem7  10277  isf34lem7  10297  isf34lem6  10298  acncc  10358  axdc2lem  10366  axdc3lem2  10369  axdc3lem4  10371  axdc4lem  10373  axcclem  10375  ttukeylem6  10432  alephreg  10501  pwcfsdom  10502  canthp1lem2  10572  canthp1  10573  pwfseqlem1  10577  pwfseqlem4a  10580  gruf  10730  fsequb2  13933  axdc4uzlem  13940  seqf1o  14000  hashf1lem1  14412  wwlktovf  14913  shftf  15036  limsupgre  15438  rlimuni  15507  lo1resb  15521  o1resb  15523  o1of2  15570  o1rlimmul  15576  isercolllem1  15622  isercolllem2  15623  isercolllem3  15624  isercoll  15625  climsup  15627  iseralt  15642  sumeq2ii  15650  summolem2a  15672  isumcl  15718  isumshft  15799  climcndslem2  15810  climcnds  15811  mertenslem2  15845  prodeq2ii  15871  prodmolem2a  15894  iprodcl  15961  rpnnen2lem10  16185  ruclem8  16199  ruclem12  16203  3dvds  16295  smueqlem  16454  nn0seqcvgd  16534  algrf  16537  eucalg  16551  phimullem  16744  pcmpt  16858  pcprod  16861  vdwlem11  16957  vdwnnlem3  16963  ramlb  16985  0ram  16986  ramcl  16995  prmgaplem8  17024  imasaddfnlem  17487  imasaddflem  17489  chnpof1  18591  mgmhmpropd  18661  mhmpropd  18755  smndex1gid  18867  smndex1gidOLD  18868  ghmsub  19193  cntzmhm  19310  f1omvdconj  19415  pj1ghm  19672  gsumzaddlem  19890  gsumzadd  19891  gsummptnn0fzfv  19956  dprdfadd  19991  subgdmdprd  20005  gsumdixp  20292  lspcl  20969  znunit  21541  frlmsslsp  21774  frlmup2  21777  lindfmm  21805  islindf4  21816  psrbaglesupp  21900  psrbaglefi  21904  resspsrmul  21953  evlslem4  22055  evlslem3  22059  fvcoe1  22195  psropprmul  22225  00ply1bas  22227  subrgvr1cl  22251  coe1mul2lem1  22256  coe1tmmul  22266  ply1coe  22287  evl1val  22318  evl1sca  22323  pf1const  22335  1mavmul  22534  mavmulass  22535  marepvcl  22555  1marepvmarrepid  22561  cramerimplem1  22669  pmatcollpw3fi1lem1  22772  pmatcollpw3fi1lem2  22773  cpmadugsumlemF  22862  cpmadugsumfi  22863  cayleyhamilton1  22878  hauscmplem  23392  ptbasid  23561  ptpjcn  23597  upxp  23609  uptx  23611  txcmplem2  23628  xkopt  23641  txhmeo  23789  alexsubALTlem3  24035  nrginvrcn  24678  nmoi  24714  nmoleub  24717  cncfmet  24897  cnheibor  24943  evth  24947  pcopt  25010  pcopt2  25011  pcorevlem  25014  pi1xfrf  25041  pi1xfr  25043  pi1xfrcnvlem  25044  iscauf  25268  iscmet3lem1  25279  iscmet3lem2  25280  iscmet3  25281  causs  25286  bcthlem5  25316  bcth3  25319  ovolfcl  25454  ovolfioo  25455  ovolficc  25456  ovolficcss  25457  ovolfsval  25458  ovolmge0  25465  ovollb2lem  25476  ovolunlem1a  25484  ovoliunlem1  25490  ovoliunlem2  25491  ovoliun  25493  ovolicc1  25504  ovolicc2lem3  25507  ovolicc2lem4  25508  ovolicc2lem5  25509  voliunlem1  25538  volsup  25544  ioombl1lem2  25547  ovolfs2  25559  uniioovol  25567  uniiccvol  25568  uniioombllem3a  25572  uniioombllem3  25573  uniioombllem4  25574  uniioombllem5  25575  uniioombllem6  25576  dyadmbl  25588  volcn  25594  ismbf  25616  mbfadd  25649  mbfsub  25650  mbflimsup  25654  0plef  25660  itg1climres  25702  mbfi1fseqlem1  25703  mbfi1fseqlem3  25705  mbfi1fseqlem4  25706  mbfi1fseqlem5  25707  mbfmul  25714  xrge0f  25719  itg2ge0  25723  itg2seq  25730  itg2uba  25731  itg2lea  25732  itg2eqa  25733  itg2splitlem  25736  itg2split  25737  itg2i1fseqle  25742  itg2i1fseq  25743  itg2i1fseq2  25744  itg2addlem  25746  bddmulibl  25827  ellimc3  25867  dvaddbr  25926  dvcobr  25934  dvcj  25938  dvfre  25939  dvcnvlem  25964  dvlip  25981  dvlipcn  25982  c1lip1  25985  tdeglem4  26046  tdeglem2  26047  coe1mul3  26085  ply1rem  26152  fta1g  26156  ig1pdvds  26166  plyf  26184  plyeq0lem  26196  plypf1  26198  plyaddlem  26201  plymullem  26202  plyco  26227  dgreq  26230  0dgrb  26232  coefv0  26234  coeaddlem  26235  coemullem  26236  coemulc  26241  plycn  26247  dgrcolem2  26260  plycjlem  26262  plycj  26263  plycjOLD  26265  plyrecj  26267  plyreres  26270  dvply1  26271  vieta1lem2  26298  vieta1  26299  elqaalem2  26307  aareccl  26313  aalioulem1  26319  ulmcaulem  26380  ulmcau  26381  ulmcn  26385  mtest  26390  psergf  26398  dvradcnv  26407  psercn2  26409  pserdvlem2  26414  pserdv2  26416  abelthlem6  26422  abelthlem8  26425  abelthlem9  26426  logtayl  26645  amgm  26975  ftalem1  27057  ftalem2  27058  ftalem3  27059  ftalem4  27060  ftalem5  27061  basellem2  27066  muinv  27177  dchrmulcl  27233  dchrinvcl  27237  dchrfi  27239  dchrghm  27240  dchrsum2  27252  dchrsum  27253  bposlem5  27272  lgscllem  27288  lgsval4a  27303  lgsneg  27305  lgsdir  27316  lgsdilem2  27317  lgsdi  27318  lgsne0  27319  lgseisenlem3  27361  rpvmasumlem  27471  dchrmusum2  27478  dchrvmasumiflem1  27485  dchrisum0ff  27491  dchrisum0flblem1  27492  dchrisum0fno1  27495  rpvmasum2  27496  dchrisum0re  27497  dchrisum0lem2a  27501  upgrreslem  29393  umgrreslem  29394  wlkpvtx  29746  wlkepvtx  29747  usgr2pthlem  29851  frgrncvvdeqlem8  30396  lnoadd  30849  lnosub  30850  nmosetre  30855  nmooge0  30858  nmoub3i  30864  nmounbi  30867  phoeqi  30948  ubthlem1  30961  h2hcau  31070  h2hlm  31071  hoscl  31836  homcl  31837  hodcl  31838  hoaddcl  31849  homulcl  31850  homullid  31891  homco1  31892  homulass  31893  hoadddi  31894  hoadddir  31895  hoeq1  31921  hoeq2  31922  adjsym  31924  nmopsetretALT  31954  nmfnsetre  31968  cnvadj  31983  hhcno  31995  hhcnf  31996  nmopub2tALT  32000  nmopge0  32002  unopf1o  32007  unoplin  32011  counop  32012  nmfnleub2  32017  nmfnge0  32018  hmoplin  32033  eigvalcl  32052  lnop0  32057  hmops  32111  hmopm  32112  nlelchi  32152  leop2  32215  leopadd  32223  leopmuli  32224  leopnmid  32229  hmopidmchi  32242  pjinvari  32282  sticl  32306  fcomptf  32752  rge0scvg  34143  esumcst  34257  esumfzf  34263  esumfsup  34264  esumfsupre  34265  hasheuni  34279  measdivcstALTV  34419  eulerpartlems  34554  eulerpartlemgc  34556  eulerpartlemb  34562  derangsn  35411  subfacp1lem5  35425  subfacp1lem6  35426  pconnconn  35472  sconnpi1  35480  txsconnlem  35481  cvxsconn  35484  cvmliftphtlem  35558  cvmlift3lem2  35561  cvmlift3lem4  35563  cvmlift3lem6  35565  satfvel  35653  satefvfmla1  35666  elmrsubrn  35761  msubff  35771  msubvrs  35801  mclsssvlem  35803  faclim  35987  curf  37978  uncf  37979  curunc  37982  unccur  37983  matunitlindflem1  37996  matunitlindflem2  37997  ptrecube  38000  heicant  38035  mblfinlem2  38038  itg2addnclem  38051  ftc1anclem1  38073  ftc1anclem2  38074  ftc1anclem4  38076  upixp  38109  fdc  38125  seqpo  38127  incsequz  38128  incsequz2  38129  metf1o  38135  geomcau  38139  sstotbnd2  38154  prdsbnd  38173  ismtyima  38183  ismtyhmeolem  38184  heiborlem3  38193  heiborlem6  38196  heiborlem10  38200  bfplem1  38202  ghomco  38271  sticksstones11  42654  mzpclall  43189  mzprename  43211  rexrabdioph  43252  rmydioph  43472  rmxdioph  43474  expdiophlem2  43480  expdioph  43481  pw2f1ocnv  43495  kelac1  43521  rngunsnply  43627  ofsubid  44781  ofdivrec  44783  ofdivcan4  44784  ofdivdiv2  44785  dvconstbi  44791  refsum2cnlem1  45498  climinf  46063  stoweidlem26  46481  stoweidlem60  46515  stoweid  46518  dmvolsal  46801  caratheodory  46983  elhoi  46997  smfresal  47243  f1oresf1o2  47766  fargshiftf  47927  nnsum4primeseven  48303  nnsum4primesevenALTV  48304  isubgrvtxuhgr  48367  isubgruhgr  48371  isubgr0uhgr  48376  grimuhgr  48390  gricushgr  48420  rmsupp0  48871  domnmsuppn0  48872  gsumlsscl  48883  lincfsuppcl  48916  linccl  48917  lincdifsn  48927  lincsum  48932  lincscm  48933  lincscmcl  48935  lincext1  48957  lindslinindimp2lem1  48961  lindslinindimp2lem4  48964  lindslinindsimp2lem5  48965  snlindsntor  48974  lincresunitlem2  48979  lincresunit3lem1  48982  lincresunit3lem2  48983  lincresunit3  48984  lincreslvec3  48985  isldepslvec2  48988  zlmodzxzldeplem3  49005  1arympt1  49141  ackendofnn0  49187  xpco2  49359  aacllem  50303