Theorem ffvelcdm 6987

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 6626	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 6986	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 580	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6633	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3924	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 481	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2103  ran crn 5597   Fn wfn 6449  ⟶wf 6450  ‘cfv 6454

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-10 2134  ax-12 2168  ax-ext 2706  ax-sep 5231  ax-nul 5238  ax-pr 5360

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1541  df-fal 1551  df-ex 1779  df-nf 1783  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2727  df-clel 2813  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3226  df-v 3438  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4844  df-br 5081  df-opab 5143  df-id 5496  df-xp 5602  df-rel 5603  df-cnv 5604  df-co 5605  df-dm 5606  df-rn 5607  df-iota 6406  df-fun 6456  df-fn 6457  df-f 6458  df-fv 6462

This theorem is referenced by:  ffvelcdmi  6988  ffvelcdmda  6989  dffo3  7006  foco2  7011  ffnfv  7020  ffvresb  7026  fcompt  7033  fsn2  7036  fvconst  7064  fprb  7097  f1cofveqaeq  7159  2f1fvneq  7161  fcofo  7188  cocan1  7191  isocnv  7229  isocnv3  7231  isores2  7232  isopolem  7244  isosolem  7246  fovcdm  7470  off  7579  fnwelem  8000  smofvon2  8215  smorndom  8227  omsmolem  8515  omsmo  8516  fsetfcdm  8676  mapfvd  8695  mapsncnv  8709  2dom  8852  xpdom2  8887  domunsncan  8892  xpmapenlem  8964  fiint  9127  infdifsn  9451  cantnflem1  9483  wemapwe  9491  cnfcom3lem  9497  updjudhf  9725  fseqenlem1  9816  finacn  9842  ackbij1lem12  10023  cofsmo  10061  cfsmolem  10062  cfcoflem  10064  coftr  10065  isf32lem6  10150  isf32lem7  10151  isf34lem7  10171  isf34lem6  10172  acncc  10232  axdc2lem  10240  axdc3lem2  10243  axdc3lem4  10245  axdc4lem  10247  axcclem  10249  ttukeylem6  10306  alephreg  10374  pwcfsdom  10375  canthp1lem2  10445  canthp1  10446  pwfseqlem1  10450  pwfseqlem4a  10453  gruf  10603  fsequb2  13732  axdc4uzlem  13739  seqf1o  13800  hashf1lem1  14203  hashf1lem1OLD  14204  wwlktovf  14706  shftf  14825  limsupgre  15225  rlimuni  15294  lo1resb  15308  o1resb  15310  o1of2  15357  o1rlimmul  15363  isercolllem1  15411  isercolllem2  15412  isercolllem3  15413  isercoll  15414  climsup  15416  iseralt  15431  sumeq2ii  15440  summolem2a  15462  isumcl  15508  isumshft  15586  climcndslem2  15597  climcnds  15598  mertenslem2  15632  prodeq2ii  15658  prodmolem2a  15679  iprodcl  15746  rpnnen2lem10  15967  ruclem8  15981  ruclem12  15985  3dvds  16075  smueqlem  16232  nn0seqcvgd  16310  algrf  16313  eucalg  16327  phimullem  16515  pcmpt  16628  pcprod  16631  vdwlem11  16727  vdwnnlem3  16733  ramlb  16755  0ram  16756  ramcl  16765  prmgaplem8  16794  imasaddfnlem  17274  imasaddflem  17276  mhmpropd  18471  smndex1gid  18577  ghmsub  18877  cntzmhm  18980  f1omvdconj  19089  pj1ghm  19344  gsumzaddlem  19557  gsumzadd  19558  gsummptnn0fzfv  19623  dprdfadd  19658  subgdmdprd  19672  gsumdixp  19883  lspcl  20273  znunit  20806  frlmsslsp  21038  frlmup2  21041  lindfmm  21069  islindf4  21080  psrbaglesupp  21162  psrbaglesuppOLD  21163  psrbaglefi  21170  psrbaglefiOLD  21171  resspsrmul  21221  evlslem4  21319  evlslem3  21325  fvcoe1  21413  psropprmul  21444  00ply1bas  21446  subrgvr1cl  21468  coe1mul2lem1  21473  coe1tmmul  21483  ply1coe  21502  evl1val  21530  evl1sca  21535  pf1const  21547  1mavmul  21732  mavmulass  21733  marepvcl  21753  1marepvmarrepid  21759  cramerimplem1  21867  pmatcollpw3fi1lem1  21970  pmatcollpw3fi1lem2  21971  cpmadugsumlemF  22060  cpmadugsumfi  22061  cayleyhamilton1  22076  hauscmplem  22592  ptbasid  22761  ptpjcn  22797  upxp  22809  uptx  22811  txcmplem2  22828  xkopt  22841  txhmeo  22989  alexsubALTlem3  23235  nrginvrcn  23891  nmoi  23927  nmoleub  23930  cncfmet  24107  cnheibor  24153  evth  24157  pcopt  24220  pcopt2  24221  pcorevlem  24224  pi1xfrf  24251  pi1xfr  24253  pi1xfrcnvlem  24254  iscauf  24479  iscmet3lem1  24490  iscmet3lem2  24491  iscmet3  24492  causs  24497  bcthlem5  24527  bcth3  24530  ovolfcl  24665  ovolfioo  24666  ovolficc  24667  ovolficcss  24668  ovolfsval  24669  ovolmge0  24676  ovollb2lem  24687  ovolunlem1a  24695  ovoliunlem1  24701  ovoliunlem2  24702  ovoliun  24704  ovolicc1  24715  ovolicc2lem3  24718  ovolicc2lem4  24719  ovolicc2lem5  24720  voliunlem1  24749  volsup  24755  ioombl1lem2  24758  ovolfs2  24770  uniioovol  24778  uniiccvol  24779  uniioombllem3a  24783  uniioombllem3  24784  uniioombllem4  24785  uniioombllem5  24786  uniioombllem6  24787  dyadmbl  24799  volcn  24805  ismbf  24827  mbfadd  24860  mbfsub  24861  mbflimsup  24865  0plef  24871  itg1climres  24914  mbfi1fseqlem1  24915  mbfi1fseqlem3  24917  mbfi1fseqlem4  24918  mbfi1fseqlem5  24919  mbfmul  24926  xrge0f  24931  itg2ge0  24935  itg2seq  24942  itg2uba  24943  itg2lea  24944  itg2eqa  24945  itg2splitlem  24948  itg2split  24949  itg2i1fseqle  24954  itg2i1fseq  24955  itg2i1fseq2  24956  itg2addlem  24958  bddmulibl  25038  ellimc3  25078  dvaddbr  25137  dvcobr  25145  dvcj  25149  dvfre  25150  dvcnvlem  25175  dvlip  25192  dvlipcn  25193  c1lip1  25196  tdeglem4  25259  tdeglem4OLD  25260  tdeglem2  25261  coe1mul3  25299  ply1rem  25363  fta1g  25367  ig1pdvds  25376  plyf  25394  plyeq0lem  25406  plypf1  25408  plyaddlem  25411  plymullem  25412  plyco  25437  dgreq  25440  0dgrb  25442  coefv0  25444  coeaddlem  25445  coemullem  25446  coemulc  25451  plycn  25457  dgrcolem2  25470  plycjlem  25472  plycj  25473  plyrecj  25475  plyreres  25478  dvply1  25479  vieta1lem2  25506  vieta1  25507  elqaalem2  25515  aareccl  25521  aalioulem1  25527  ulmcaulem  25588  ulmcau  25589  ulmcn  25593  mtest  25598  psergf  25606  dvradcnv  25615  psercn2  25617  pserdvlem2  25622  pserdv2  25624  abelthlem6  25630  abelthlem8  25633  abelthlem9  25634  logtayl  25850  amgm  26175  ftalem1  26257  ftalem2  26258  ftalem3  26259  ftalem4  26260  ftalem5  26261  basellem2  26266  muinv  26377  dchrmulcl  26432  dchrinvcl  26436  dchrfi  26438  dchrghm  26439  dchrsum2  26451  dchrsum  26452  bposlem5  26471  lgscllem  26487  lgsval4a  26502  lgsneg  26504  lgsdir  26515  lgsdilem2  26516  lgsdi  26517  lgsne0  26518  lgseisenlem3  26560  rpvmasumlem  26670  dchrmusum2  26677  dchrvmasumiflem1  26684  dchrisum0ff  26690  dchrisum0flblem1  26691  dchrisum0fno1  26694  rpvmasum2  26695  dchrisum0re  26696  dchrisum0lem2a  26700  upgrreslem  27706  umgrreslem  27707  wlkpvtx  28062  wlkepvtx  28063  usgr2pthlem  28166  frgrncvvdeqlem8  28705  lnoadd  29155  lnosub  29156  nmosetre  29161  nmooge0  29164  nmoub3i  29170  nmounbi  29173  phoeqi  29254  ubthlem1  29267  h2hcau  29376  h2hlm  29377  hoscl  30142  homcl  30143  hodcl  30144  hoaddcl  30155  homulcl  30156  homulid2  30197  homco1  30198  homulass  30199  hoadddi  30200  hoadddir  30201  hoeq1  30227  hoeq2  30228  adjsym  30230  nmopsetretALT  30260  nmfnsetre  30274  cnvadj  30289  hhcno  30301  hhcnf  30302  nmopub2tALT  30306  nmopge0  30308  unopf1o  30313  unoplin  30317  counop  30318  nmfnleub2  30323  nmfnge0  30324  hmoplin  30339  eigvalcl  30358  lnop0  30363  hmops  30417  hmopm  30418  nlelchi  30458  leop2  30521  leopadd  30529  leopmuli  30530  leopnmid  30535  hmopidmchi  30548  pjinvari  30588  sticl  30612  fcomptf  31030  rge0scvg  31934  esumcst  32066  esumfzf  32072  esumfsup  32073  esumfsupre  32074  hasheuni  32088  measdivcstALTV  32228  eulerpartlems  32362  eulerpartlemgc  32364  eulerpartlemb  32370  derangsn  33167  subfacp1lem5  33181  subfacp1lem6  33182  pconnconn  33228  sconnpi1  33236  txsconnlem  33237  cvxsconn  33240  cvmliftphtlem  33314  cvmlift3lem2  33317  cvmlift3lem4  33319  cvmlift3lem6  33321  satfvel  33409  satefvfmla1  33422  elmrsubrn  33517  msubff  33527  msubvrs  33557  mclsssvlem  33559  faclim  33747  soseq  33838  curf  35790  uncf  35791  curunc  35794  unccur  35795  matunitlindflem1  35808  matunitlindflem2  35809  ptrecube  35812  heicant  35847  mblfinlem2  35850  itg2addnclem  35863  ftc1anclem1  35885  ftc1anclem2  35886  ftc1anclem4  35888  upixp  35922  fdc  35938  seqpo  35940  incsequz  35941  incsequz2  35942  metf1o  35948  geomcau  35952  sstotbnd2  35967  prdsbnd  35986  ismtyima  35996  ismtyhmeolem  35997  heiborlem3  36006  heiborlem6  36009  heiborlem10  36013  bfplem1  36015  ghomco  36084  sticksstones11  40145  mzpclall  40579  mzprename  40601  rexrabdioph  40646  rmydioph  40867  rmxdioph  40869  expdiophlem2  40875  expdioph  40876  pw2f1ocnv  40890  kelac1  40919  rngunsnply  41029  ofsubid  41973  ofdivrec  41975  ofdivcan4  41976  ofdivdiv2  41977  dvconstbi  41983  refsum2cnlem1  42611  dffo3f  42754  climinf  43189  stoweidlem26  43609  stoweidlem60  43643  stoweid  43646  dmvolsal  43927  caratheodory  44109  elhoi  44123  smfresal  44369  f1oresf1o2  44830  fargshiftf  44939  nnsum4primeseven  45299  nnsum4primesevenALTV  45300  isomushgr  45325  isomgrtrlem  45337  mgmhmpropd  45386  rmsupp0  45751  domnmsuppn0  45752  gsumlsscl  45766  lincfsuppcl  45801  linccl  45802  lincdifsn  45812  lincsum  45817  lincscm  45818  lincscmcl  45820  lincext1  45842  lindslinindimp2lem1  45846  lindslinindimp2lem4  45849  lindslinindsimp2lem5  45850  snlindsntor  45859  lincresunitlem2  45864  lincresunit3lem1  45867  lincresunit3lem2  45868  lincresunit3  45869  lincreslvec3  45870  isldepslvec2  45873  zlmodzxzldeplem3  45890  1arympt1  46031  ackendofnn0  46077  aacllem  46552