Theorem ffvelcdm 7028

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ran crn 5626   Fn wfn 6488  ⟶wf 6489  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2709  ax-sep 5242  ax-nul 5252  ax-pr 5378

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501

This theorem is referenced by:  ffvelcdmi  7030  ffvelcdmda  7031  dffo3  7049  dffo3f  7053  foco2  7056  ffnfv  7066  ffvresb  7072  fcompt  7080  fsn2  7083  fvconst  7110  fprb  7142  f1cofveqaeq  7205  fcofo  7236  cocan1  7239  fvf1pr  7255  isocnv  7278  isocnv3  7280  isores2  7281  isopolem  7293  isosolem  7295  fovcdm  7530  off  7642  fnwelem  8075  soseq  8103  smofvon2  8290  smocdmdom  8302  omsmolem  8587  omsmo  8588  fsetfcdm  8801  mapfvd  8821  mapsncnv  8835  2dom  8971  xpdom2  9004  domunsncan  9009  xpmapenlem  9076  fiint  9231  infdifsn  9570  cantnflem1  9602  wemapwe  9610  cnfcom3lem  9616  updjudhf  9847  fseqenlem1  9938  finacn  9964  ackbij1lem12  10144  cofsmo  10183  cfsmolem  10184  cfcoflem  10186  coftr  10187  isf32lem6  10272  isf32lem7  10273  isf34lem7  10293  isf34lem6  10294  acncc  10354  axdc2lem  10362  axdc3lem2  10365  axdc3lem4  10367  axdc4lem  10369  axcclem  10371  ttukeylem6  10428  alephreg  10497  pwcfsdom  10498  canthp1lem2  10568  canthp1  10569  pwfseqlem1  10573  pwfseqlem4a  10576  gruf  10726  fsequb2  13903  axdc4uzlem  13910  seqf1o  13970  hashf1lem1  14382  wwlktovf  14883  shftf  15006  limsupgre  15408  rlimuni  15477  lo1resb  15491  o1resb  15493  o1of2  15540  o1rlimmul  15546  isercolllem1  15592  isercolllem2  15593  isercolllem3  15594  isercoll  15595  climsup  15597  iseralt  15612  sumeq2ii  15620  summolem2a  15642  isumcl  15688  isumshft  15766  climcndslem2  15777  climcnds  15778  mertenslem2  15812  prodeq2ii  15838  prodmolem2a  15861  iprodcl  15928  rpnnen2lem10  16152  ruclem8  16166  ruclem12  16170  3dvds  16262  smueqlem  16421  nn0seqcvgd  16501  algrf  16504  eucalg  16518  phimullem  16710  pcmpt  16824  pcprod  16827  vdwlem11  16923  vdwnnlem3  16929  ramlb  16951  0ram  16952  ramcl  16961  prmgaplem8  16990  imasaddfnlem  17453  imasaddflem  17455  chnpof1  18557  mgmhmpropd  18627  mhmpropd  18721  smndex1gid  18832  ghmsub  19157  cntzmhm  19274  f1omvdconj  19379  pj1ghm  19636  gsumzaddlem  19854  gsumzadd  19855  gsummptnn0fzfv  19920  dprdfadd  19955  subgdmdprd  19969  gsumdixp  20258  lspcl  20931  znunit  21522  frlmsslsp  21755  frlmup2  21758  lindfmm  21786  islindf4  21797  psrbaglesupp  21882  psrbaglefi  21886  resspsrmul  21935  evlslem4  22035  evlslem3  22039  fvcoe1  22152  psropprmul  22182  00ply1bas  22184  subrgvr1cl  22208  coe1mul2lem1  22213  coe1tmmul  22223  ply1coe  22246  evl1val  22277  evl1sca  22282  pf1const  22294  1mavmul  22496  mavmulass  22497  marepvcl  22517  1marepvmarrepid  22523  cramerimplem1  22631  pmatcollpw3fi1lem1  22734  pmatcollpw3fi1lem2  22735  cpmadugsumlemF  22824  cpmadugsumfi  22825  cayleyhamilton1  22840  hauscmplem  23354  ptbasid  23523  ptpjcn  23559  upxp  23571  uptx  23573  txcmplem2  23590  xkopt  23603  txhmeo  23751  alexsubALTlem3  23997  nrginvrcn  24640  nmoi  24676  nmoleub  24679  cncfmet  24862  cnheibor  24914  evth  24918  pcopt  24982  pcopt2  24983  pcorevlem  24986  pi1xfrf  25013  pi1xfr  25015  pi1xfrcnvlem  25016  iscauf  25240  iscmet3lem1  25251  iscmet3lem2  25252  iscmet3  25253  causs  25258  bcthlem5  25288  bcth3  25291  ovolfcl  25427  ovolfioo  25428  ovolficc  25429  ovolficcss  25430  ovolfsval  25431  ovolmge0  25438  ovollb2lem  25449  ovolunlem1a  25457  ovoliunlem1  25463  ovoliunlem2  25464  ovoliun  25466  ovolicc1  25477  ovolicc2lem3  25480  ovolicc2lem4  25481  ovolicc2lem5  25482  voliunlem1  25511  volsup  25517  ioombl1lem2  25520  ovolfs2  25532  uniioovol  25540  uniiccvol  25541  uniioombllem3a  25545  uniioombllem3  25546  uniioombllem4  25547  uniioombllem5  25548  uniioombllem6  25549  dyadmbl  25561  volcn  25567  ismbf  25589  mbfadd  25622  mbfsub  25623  mbflimsup  25627  0plef  25633  itg1climres  25675  mbfi1fseqlem1  25676  mbfi1fseqlem3  25678  mbfi1fseqlem4  25679  mbfi1fseqlem5  25680  mbfmul  25687  xrge0f  25692  itg2ge0  25696  itg2seq  25703  itg2uba  25704  itg2lea  25705  itg2eqa  25706  itg2splitlem  25709  itg2split  25710  itg2i1fseqle  25715  itg2i1fseq  25716  itg2i1fseq2  25717  itg2addlem  25719  bddmulibl  25800  ellimc3  25840  dvaddbr  25900  dvcobr  25909  dvcobrOLD  25910  dvcj  25914  dvfre  25915  dvcnvlem  25940  dvlip  25958  dvlipcn  25959  c1lip1  25962  tdeglem4  26025  tdeglem2  26026  coe1mul3  26064  ply1rem  26131  fta1g  26135  ig1pdvds  26145  plyf  26163  plyeq0lem  26175  plypf1  26177  plyaddlem  26180  plymullem  26181  plyco  26206  dgreq  26209  0dgrb  26211  coefv0  26213  coeaddlem  26214  coemullem  26215  coemulc  26220  plycn  26226  plycnOLD  26227  dgrcolem2  26240  plycjlem  26242  plycj  26243  plycjOLD  26245  plyrecj  26247  plyreres  26250  dvply1  26251  vieta1lem2  26279  vieta1  26280  elqaalem2  26288  aareccl  26294  aalioulem1  26300  ulmcaulem  26363  ulmcau  26364  ulmcn  26368  mtest  26373  psergf  26381  dvradcnv  26390  psercn2  26392  psercn2OLD  26393  pserdvlem2  26398  pserdv2  26400  abelthlem6  26406  abelthlem8  26409  abelthlem9  26410  logtayl  26629  amgm  26961  ftalem1  27043  ftalem2  27044  ftalem3  27045  ftalem4  27046  ftalem5  27047  basellem2  27052  muinv  27163  dchrmulcl  27220  dchrinvcl  27224  dchrfi  27226  dchrghm  27227  dchrsum2  27239  dchrsum  27240  bposlem5  27259  lgscllem  27275  lgsval4a  27290  lgsneg  27292  lgsdir  27303  lgsdilem2  27304  lgsdi  27305  lgsne0  27306  lgseisenlem3  27348  rpvmasumlem  27458  dchrmusum2  27465  dchrvmasumiflem1  27472  dchrisum0ff  27478  dchrisum0flblem1  27479  dchrisum0fno1  27482  rpvmasum2  27483  dchrisum0re  27484  dchrisum0lem2a  27488  upgrreslem  29381  umgrreslem  29382  wlkpvtx  29735  wlkepvtx  29736  usgr2pthlem  29840  frgrncvvdeqlem8  30385  lnoadd  30837  lnosub  30838  nmosetre  30843  nmooge0  30846  nmoub3i  30852  nmounbi  30855  phoeqi  30936  ubthlem1  30949  h2hcau  31058  h2hlm  31059  hoscl  31824  homcl  31825  hodcl  31826  hoaddcl  31837  homulcl  31838  homullid  31879  homco1  31880  homulass  31881  hoadddi  31882  hoadddir  31883  hoeq1  31909  hoeq2  31910  adjsym  31912  nmopsetretALT  31942  nmfnsetre  31956  cnvadj  31971  hhcno  31983  hhcnf  31984  nmopub2tALT  31988  nmopge0  31990  unopf1o  31995  unoplin  31999  counop  32000  nmfnleub2  32005  nmfnge0  32006  hmoplin  32021  eigvalcl  32040  lnop0  32045  hmops  32099  hmopm  32100  nlelchi  32140  leop2  32203  leopadd  32211  leopmuli  32212  leopnmid  32217  hmopidmchi  32230  pjinvari  32270  sticl  32294  fcomptf  32739  rge0scvg  34108  esumcst  34222  esumfzf  34228  esumfsup  34229  esumfsupre  34230  hasheuni  34244  measdivcstALTV  34384  eulerpartlems  34519  eulerpartlemgc  34521  eulerpartlemb  34527  derangsn  35366  subfacp1lem5  35380  subfacp1lem6  35381  pconnconn  35427  sconnpi1  35435  txsconnlem  35436  cvxsconn  35439  cvmliftphtlem  35513  cvmlift3lem2  35516  cvmlift3lem4  35518  cvmlift3lem6  35520  satfvel  35608  satefvfmla1  35621  elmrsubrn  35716  msubff  35726  msubvrs  35756  mclsssvlem  35758  faclim  35942  curf  37801  uncf  37802  curunc  37805  unccur  37806  matunitlindflem1  37819  matunitlindflem2  37820  ptrecube  37823  heicant  37858  mblfinlem2  37861  itg2addnclem  37874  ftc1anclem1  37896  ftc1anclem2  37897  ftc1anclem4  37899  upixp  37932  fdc  37948  seqpo  37950  incsequz  37951  incsequz2  37952  metf1o  37958  geomcau  37962  sstotbnd2  37977  prdsbnd  37996  ismtyima  38006  ismtyhmeolem  38007  heiborlem3  38016  heiborlem6  38019  heiborlem10  38023  bfplem1  38025  ghomco  38094  sticksstones11  42478  mzpclall  43036  mzprename  43058  rexrabdioph  43103  rmydioph  43323  rmxdioph  43325  expdiophlem2  43331  expdioph  43332  pw2f1ocnv  43346  kelac1  43372  rngunsnply  43478  ofsubid  44632  ofdivrec  44634  ofdivcan4  44635  ofdivdiv2  44636  dvconstbi  44642  refsum2cnlem1  45349  climinf  45919  stoweidlem26  46337  stoweidlem60  46371  stoweid  46374  dmvolsal  46657  caratheodory  46839  elhoi  46853  smfresal  47099  f1oresf1o2  47604  fargshiftf  47753  nnsum4primeseven  48113  nnsum4primesevenALTV  48114  isubgrvtxuhgr  48177  isubgruhgr  48181  isubgr0uhgr  48186  grimuhgr  48200  gricushgr  48230  rmsupp0  48681  domnmsuppn0  48682  gsumlsscl  48693  lincfsuppcl  48726  linccl  48727  lincdifsn  48737  lincsum  48742  lincscm  48743  lincscmcl  48745  lincext1  48767  lindslinindimp2lem1  48771  lindslinindimp2lem4  48774  lindslinindsimp2lem5  48775  snlindsntor  48784  lincresunitlem2  48789  lincresunit3lem1  48792  lincresunit3lem2  48793  lincresunit3  48794  lincreslvec3  48795  isldepslvec2  48798  zlmodzxzldeplem3  48815  1arympt1  48951  ackendofnn0  48997  xpco2  49169  aacllem  50113