Theorem ffvelcdm 7015

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5620   Fn wfn 6477  ⟶wf 6478  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-fv 6490

This theorem is referenced by:  ffvelcdmi  7017  ffvelcdmda  7018  dffo3  7036  dffo3f  7040  foco2  7043  ffnfv  7053  ffvresb  7059  fcompt  7067  fsn2  7070  fvconst  7098  fprb  7130  f1cofveqaeq  7194  fcofo  7225  cocan1  7228  fvf1pr  7244  isocnv  7267  isocnv3  7269  isores2  7270  isopolem  7282  isosolem  7284  fovcdm  7519  off  7631  fnwelem  8064  soseq  8092  smofvon2  8279  smocdmdom  8291  omsmolem  8575  omsmo  8576  fsetfcdm  8787  mapfvd  8806  mapsncnv  8820  2dom  8955  xpdom2  8989  domunsncan  8994  xpmapenlem  9061  fiint  9216  fiintOLD  9217  infdifsn  9553  cantnflem1  9585  wemapwe  9593  cnfcom3lem  9599  updjudhf  9827  fseqenlem1  9918  finacn  9944  ackbij1lem12  10124  cofsmo  10163  cfsmolem  10164  cfcoflem  10166  coftr  10167  isf32lem6  10252  isf32lem7  10253  isf34lem7  10273  isf34lem6  10274  acncc  10334  axdc2lem  10342  axdc3lem2  10345  axdc3lem4  10347  axdc4lem  10349  axcclem  10351  ttukeylem6  10408  alephreg  10476  pwcfsdom  10477  canthp1lem2  10547  canthp1  10548  pwfseqlem1  10552  pwfseqlem4a  10555  gruf  10705  fsequb2  13883  axdc4uzlem  13890  seqf1o  13950  hashf1lem1  14362  wwlktovf  14863  shftf  14986  limsupgre  15388  rlimuni  15457  lo1resb  15471  o1resb  15473  o1of2  15520  o1rlimmul  15526  isercolllem1  15572  isercolllem2  15573  isercolllem3  15574  isercoll  15575  climsup  15577  iseralt  15592  sumeq2ii  15600  summolem2a  15622  isumcl  15668  isumshft  15746  climcndslem2  15757  climcnds  15758  mertenslem2  15792  prodeq2ii  15818  prodmolem2a  15841  iprodcl  15908  rpnnen2lem10  16132  ruclem8  16146  ruclem12  16150  3dvds  16242  smueqlem  16401  nn0seqcvgd  16481  algrf  16484  eucalg  16498  phimullem  16690  pcmpt  16804  pcprod  16807  vdwlem11  16903  vdwnnlem3  16909  ramlb  16931  0ram  16932  ramcl  16941  prmgaplem8  16970  imasaddfnlem  17432  imasaddflem  17434  mgmhmpropd  18572  mhmpropd  18666  smndex1gid  18777  ghmsub  19103  cntzmhm  19220  f1omvdconj  19325  pj1ghm  19582  gsumzaddlem  19800  gsumzadd  19801  gsummptnn0fzfv  19866  dprdfadd  19901  subgdmdprd  19915  gsumdixp  20204  lspcl  20879  znunit  21470  frlmsslsp  21703  frlmup2  21706  lindfmm  21734  islindf4  21745  psrbaglesupp  21829  psrbaglefi  21833  resspsrmul  21883  evlslem4  21981  evlslem3  21985  fvcoe1  22090  psropprmul  22120  00ply1bas  22122  subrgvr1cl  22146  coe1mul2lem1  22151  coe1tmmul  22161  ply1coe  22183  evl1val  22214  evl1sca  22219  pf1const  22231  1mavmul  22433  mavmulass  22434  marepvcl  22454  1marepvmarrepid  22460  cramerimplem1  22568  pmatcollpw3fi1lem1  22671  pmatcollpw3fi1lem2  22672  cpmadugsumlemF  22761  cpmadugsumfi  22762  cayleyhamilton1  22777  hauscmplem  23291  ptbasid  23460  ptpjcn  23496  upxp  23508  uptx  23510  txcmplem2  23527  xkopt  23540  txhmeo  23688  alexsubALTlem3  23934  nrginvrcn  24578  nmoi  24614  nmoleub  24617  cncfmet  24800  cnheibor  24852  evth  24856  pcopt  24920  pcopt2  24921  pcorevlem  24924  pi1xfrf  24951  pi1xfr  24953  pi1xfrcnvlem  24954  iscauf  25178  iscmet3lem1  25189  iscmet3lem2  25190  iscmet3  25191  causs  25196  bcthlem5  25226  bcth3  25229  ovolfcl  25365  ovolfioo  25366  ovolficc  25367  ovolficcss  25368  ovolfsval  25369  ovolmge0  25376  ovollb2lem  25387  ovolunlem1a  25395  ovoliunlem1  25401  ovoliunlem2  25402  ovoliun  25404  ovolicc1  25415  ovolicc2lem3  25418  ovolicc2lem4  25419  ovolicc2lem5  25420  voliunlem1  25449  volsup  25455  ioombl1lem2  25458  ovolfs2  25470  uniioovol  25478  uniiccvol  25479  uniioombllem3a  25483  uniioombllem3  25484  uniioombllem4  25485  uniioombllem5  25486  uniioombllem6  25487  dyadmbl  25499  volcn  25505  ismbf  25527  mbfadd  25560  mbfsub  25561  mbflimsup  25565  0plef  25571  itg1climres  25613  mbfi1fseqlem1  25614  mbfi1fseqlem3  25616  mbfi1fseqlem4  25617  mbfi1fseqlem5  25618  mbfmul  25625  xrge0f  25630  itg2ge0  25634  itg2seq  25641  itg2uba  25642  itg2lea  25643  itg2eqa  25644  itg2splitlem  25647  itg2split  25648  itg2i1fseqle  25653  itg2i1fseq  25654  itg2i1fseq2  25655  itg2addlem  25657  bddmulibl  25738  ellimc3  25778  dvaddbr  25838  dvcobr  25847  dvcobrOLD  25848  dvcj  25852  dvfre  25853  dvcnvlem  25878  dvlip  25896  dvlipcn  25897  c1lip1  25900  tdeglem4  25963  tdeglem2  25964  coe1mul3  26002  ply1rem  26069  fta1g  26073  ig1pdvds  26083  plyf  26101  plyeq0lem  26113  plypf1  26115  plyaddlem  26118  plymullem  26119  plyco  26144  dgreq  26147  0dgrb  26149  coefv0  26151  coeaddlem  26152  coemullem  26153  coemulc  26158  plycn  26164  plycnOLD  26165  dgrcolem2  26178  plycjlem  26180  plycj  26181  plycjOLD  26183  plyrecj  26185  plyreres  26188  dvply1  26189  vieta1lem2  26217  vieta1  26218  elqaalem2  26226  aareccl  26232  aalioulem1  26238  ulmcaulem  26301  ulmcau  26302  ulmcn  26306  mtest  26311  psergf  26319  dvradcnv  26328  psercn2  26330  psercn2OLD  26331  pserdvlem2  26336  pserdv2  26338  abelthlem6  26344  abelthlem8  26347  abelthlem9  26348  logtayl  26567  amgm  26899  ftalem1  26981  ftalem2  26982  ftalem3  26983  ftalem4  26984  ftalem5  26985  basellem2  26990  muinv  27101  dchrmulcl  27158  dchrinvcl  27162  dchrfi  27164  dchrghm  27165  dchrsum2  27177  dchrsum  27178  bposlem5  27197  lgscllem  27213  lgsval4a  27228  lgsneg  27230  lgsdir  27241  lgsdilem2  27242  lgsdi  27243  lgsne0  27244  lgseisenlem3  27286  rpvmasumlem  27396  dchrmusum2  27403  dchrvmasumiflem1  27410  dchrisum0ff  27416  dchrisum0flblem1  27417  dchrisum0fno1  27420  rpvmasum2  27421  dchrisum0re  27422  dchrisum0lem2a  27426  upgrreslem  29249  umgrreslem  29250  wlkpvtx  29603  wlkepvtx  29604  usgr2pthlem  29708  frgrncvvdeqlem8  30250  lnoadd  30702  lnosub  30703  nmosetre  30708  nmooge0  30711  nmoub3i  30717  nmounbi  30720  phoeqi  30801  ubthlem1  30814  h2hcau  30923  h2hlm  30924  hoscl  31689  homcl  31690  hodcl  31691  hoaddcl  31702  homulcl  31703  homullid  31744  homco1  31745  homulass  31746  hoadddi  31747  hoadddir  31748  hoeq1  31774  hoeq2  31775  adjsym  31777  nmopsetretALT  31807  nmfnsetre  31821  cnvadj  31836  hhcno  31848  hhcnf  31849  nmopub2tALT  31853  nmopge0  31855  unopf1o  31860  unoplin  31864  counop  31865  nmfnleub2  31870  nmfnge0  31871  hmoplin  31886  eigvalcl  31905  lnop0  31910  hmops  31964  hmopm  31965  nlelchi  32005  leop2  32068  leopadd  32076  leopmuli  32077  leopnmid  32082  hmopidmchi  32095  pjinvari  32135  sticl  32159  fcomptf  32602  rge0scvg  33922  esumcst  34036  esumfzf  34042  esumfsup  34043  esumfsupre  34044  hasheuni  34058  measdivcstALTV  34198  eulerpartlems  34334  eulerpartlemgc  34336  eulerpartlemb  34342  derangsn  35153  subfacp1lem5  35167  subfacp1lem6  35168  pconnconn  35214  sconnpi1  35222  txsconnlem  35223  cvxsconn  35226  cvmliftphtlem  35300  cvmlift3lem2  35303  cvmlift3lem4  35305  cvmlift3lem6  35307  satfvel  35395  satefvfmla1  35408  elmrsubrn  35503  msubff  35513  msubvrs  35543  mclsssvlem  35545  faclim  35729  curf  37588  uncf  37589  curunc  37592  unccur  37593  matunitlindflem1  37606  matunitlindflem2  37607  ptrecube  37610  heicant  37645  mblfinlem2  37648  itg2addnclem  37661  ftc1anclem1  37683  ftc1anclem2  37684  ftc1anclem4  37686  upixp  37719  fdc  37735  seqpo  37737  incsequz  37738  incsequz2  37739  metf1o  37745  geomcau  37749  sstotbnd2  37764  prdsbnd  37783  ismtyima  37793  ismtyhmeolem  37794  heiborlem3  37803  heiborlem6  37806  heiborlem10  37810  bfplem1  37812  ghomco  37881  sticksstones11  42139  mzpclall  42710  mzprename  42732  rexrabdioph  42777  rmydioph  42997  rmxdioph  42999  expdiophlem2  43005  expdioph  43006  pw2f1ocnv  43020  kelac1  43046  rngunsnply  43152  ofsubid  44307  ofdivrec  44309  ofdivcan4  44310  ofdivdiv2  44311  dvconstbi  44317  refsum2cnlem1  45025  climinf  45597  stoweidlem26  46017  stoweidlem60  46051  stoweid  46054  dmvolsal  46337  caratheodory  46519  elhoi  46533  smfresal  46779  f1oresf1o2  47285  fargshiftf  47434  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  isubgrvtxuhgr  47858  isubgruhgr  47862  isubgr0uhgr  47867  grimuhgr  47881  gricushgr  47911  rmsupp0  48362  domnmsuppn0  48363  gsumlsscl  48374  lincfsuppcl  48408  linccl  48409  lincdifsn  48419  lincsum  48424  lincscm  48425  lincscmcl  48427  lincext1  48449  lindslinindimp2lem1  48453  lindslinindimp2lem4  48456  lindslinindsimp2lem5  48457  snlindsntor  48466  lincresunitlem2  48471  lincresunit3lem1  48474  lincresunit3lem2  48475  lincresunit3  48476  lincreslvec3  48477  isldepslvec2  48480  zlmodzxzldeplem3  48497  1arympt1  48633  ackendofnn0  48679  xpco2  48851  aacllem  49796