Theorem ffvelcdm 7029

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ran crn 5627   Fn wfn 6489  ⟶wf 6490  ‘cfv 6494

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 5232  ax-nul 5242  ax-pr 5372

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 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502

This theorem is referenced by:  ffvelcdmi  7031  ffvelcdmda  7032  dffo3  7050  dffo3f  7054  foco2  7057  ffnfv  7067  ffvresb  7074  fcompt  7082  fsn2  7085  fvconst  7112  fprb  7144  f1cofveqaeq  7207  fcofo  7238  cocan1  7241  fvf1pr  7257  isocnv  7280  isocnv3  7282  isores2  7283  isopolem  7295  isosolem  7297  fovcdm  7532  off  7644  fnwelem  8076  soseq  8104  smofvon2  8291  smocdmdom  8303  omsmolem  8588  omsmo  8589  fsetfcdm  8802  mapfvd  8822  mapsncnv  8836  2dom  8972  xpdom2  9005  domunsncan  9010  xpmapenlem  9077  fiint  9232  infdifsn  9573  cantnflem1  9605  wemapwe  9613  cnfcom3lem  9619  updjudhf  9850  fseqenlem1  9941  finacn  9967  ackbij1lem12  10147  cofsmo  10186  cfsmolem  10187  cfcoflem  10189  coftr  10190  isf32lem6  10275  isf32lem7  10276  isf34lem7  10296  isf34lem6  10297  acncc  10357  axdc2lem  10365  axdc3lem2  10368  axdc3lem4  10370  axdc4lem  10372  axcclem  10374  ttukeylem6  10431  alephreg  10500  pwcfsdom  10501  canthp1lem2  10571  canthp1  10572  pwfseqlem1  10576  pwfseqlem4a  10579  gruf  10729  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  19194  cntzmhm  19311  f1omvdconj  19416  pj1ghm  19673  gsumzaddlem  19891  gsumzadd  19892  gsummptnn0fzfv  19957  dprdfadd  19992  subgdmdprd  20006  gsumdixp  20293  lspcl  20966  znunit  21557  frlmsslsp  21790  frlmup2  21793  lindfmm  21821  islindf4  21832  psrbaglesupp  21916  psrbaglefi  21920  resspsrmul  21968  evlslem4  22068  evlslem3  22072  fvcoe1  22185  psropprmul  22215  00ply1bas  22217  subrgvr1cl  22241  coe1mul2lem1  22246  coe1tmmul  22256  ply1coe  22277  evl1val  22308  evl1sca  22313  pf1const  22325  1mavmul  22527  mavmulass  22528  marepvcl  22548  1marepvmarrepid  22554  cramerimplem1  22662  pmatcollpw3fi1lem1  22765  pmatcollpw3fi1lem2  22766  cpmadugsumlemF  22855  cpmadugsumfi  22856  cayleyhamilton1  22871  hauscmplem  23385  ptbasid  23554  ptpjcn  23590  upxp  23602  uptx  23604  txcmplem2  23621  xkopt  23634  txhmeo  23782  alexsubALTlem3  24028  nrginvrcn  24671  nmoi  24707  nmoleub  24710  cncfmet  24890  cnheibor  24936  evth  24940  pcopt  25003  pcopt2  25004  pcorevlem  25007  pi1xfrf  25034  pi1xfr  25036  pi1xfrcnvlem  25037  iscauf  25261  iscmet3lem1  25272  iscmet3lem2  25273  iscmet3  25274  causs  25279  bcthlem5  25309  bcth3  25312  ovolfcl  25447  ovolfioo  25448  ovolficc  25449  ovolficcss  25450  ovolfsval  25451  ovolmge0  25458  ovollb2lem  25469  ovolunlem1a  25477  ovoliunlem1  25483  ovoliunlem2  25484  ovoliun  25486  ovolicc1  25497  ovolicc2lem3  25500  ovolicc2lem4  25501  ovolicc2lem5  25502  voliunlem1  25531  volsup  25537  ioombl1lem2  25540  ovolfs2  25552  uniioovol  25560  uniiccvol  25561  uniioombllem3a  25565  uniioombllem3  25566  uniioombllem4  25567  uniioombllem5  25568  uniioombllem6  25569  dyadmbl  25581  volcn  25587  ismbf  25609  mbfadd  25642  mbfsub  25643  mbflimsup  25647  0plef  25653  itg1climres  25695  mbfi1fseqlem1  25696  mbfi1fseqlem3  25698  mbfi1fseqlem4  25699  mbfi1fseqlem5  25700  mbfmul  25707  xrge0f  25712  itg2ge0  25716  itg2seq  25723  itg2uba  25724  itg2lea  25725  itg2eqa  25726  itg2splitlem  25729  itg2split  25730  itg2i1fseqle  25735  itg2i1fseq  25736  itg2i1fseq2  25737  itg2addlem  25739  bddmulibl  25820  ellimc3  25860  dvaddbr  25919  dvcobr  25927  dvcj  25931  dvfre  25932  dvcnvlem  25957  dvlip  25974  dvlipcn  25975  c1lip1  25978  tdeglem4  26039  tdeglem2  26040  coe1mul3  26078  ply1rem  26145  fta1g  26149  ig1pdvds  26159  plyf  26177  plyeq0lem  26189  plypf1  26191  plyaddlem  26194  plymullem  26195  plyco  26220  dgreq  26223  0dgrb  26225  coefv0  26227  coeaddlem  26228  coemullem  26229  coemulc  26234  plycn  26240  dgrcolem2  26253  plycjlem  26255  plycj  26256  plycjOLD  26258  plyrecj  26260  plyreres  26263  dvply1  26264  vieta1lem2  26292  vieta1  26293  elqaalem2  26301  aareccl  26307  aalioulem1  26313  ulmcaulem  26376  ulmcau  26377  ulmcn  26381  mtest  26386  psergf  26394  dvradcnv  26403  psercn2  26405  pserdvlem2  26410  pserdv2  26412  abelthlem6  26418  abelthlem8  26421  abelthlem9  26422  logtayl  26641  amgm  26972  ftalem1  27054  ftalem2  27055  ftalem3  27056  ftalem4  27057  ftalem5  27058  basellem2  27063  muinv  27174  dchrmulcl  27230  dchrinvcl  27234  dchrfi  27236  dchrghm  27237  dchrsum2  27249  dchrsum  27250  bposlem5  27269  lgscllem  27285  lgsval4a  27300  lgsneg  27302  lgsdir  27313  lgsdilem2  27314  lgsdi  27315  lgsne0  27316  lgseisenlem3  27358  rpvmasumlem  27468  dchrmusum2  27475  dchrvmasumiflem1  27482  dchrisum0ff  27488  dchrisum0flblem1  27489  dchrisum0fno1  27492  rpvmasum2  27493  dchrisum0re  27494  dchrisum0lem2a  27498  upgrreslem  29391  umgrreslem  29392  wlkpvtx  29745  wlkepvtx  29746  usgr2pthlem  29850  frgrncvvdeqlem8  30395  lnoadd  30848  lnosub  30849  nmosetre  30854  nmooge0  30857  nmoub3i  30863  nmounbi  30866  phoeqi  30947  ubthlem1  30960  h2hcau  31069  h2hlm  31070  hoscl  31835  homcl  31836  hodcl  31837  hoaddcl  31848  homulcl  31849  homullid  31890  homco1  31891  homulass  31892  hoadddi  31893  hoadddir  31894  hoeq1  31920  hoeq2  31921  adjsym  31923  nmopsetretALT  31953  nmfnsetre  31967  cnvadj  31982  hhcno  31994  hhcnf  31995  nmopub2tALT  31999  nmopge0  32001  unopf1o  32006  unoplin  32010  counop  32011  nmfnleub2  32016  nmfnge0  32017  hmoplin  32032  eigvalcl  32051  lnop0  32056  hmops  32110  hmopm  32111  nlelchi  32151  leop2  32214  leopadd  32222  leopmuli  32223  leopnmid  32228  hmopidmchi  32241  pjinvari  32281  sticl  32305  fcomptf  32750  rge0scvg  34113  esumcst  34227  esumfzf  34233  esumfsup  34234  esumfsupre  34235  hasheuni  34249  measdivcstALTV  34389  eulerpartlems  34524  eulerpartlemgc  34526  eulerpartlemb  34532  derangsn  35372  subfacp1lem5  35386  subfacp1lem6  35387  pconnconn  35433  sconnpi1  35441  txsconnlem  35442  cvxsconn  35445  cvmliftphtlem  35519  cvmlift3lem2  35522  cvmlift3lem4  35524  cvmlift3lem6  35526  satfvel  35614  satefvfmla1  35627  elmrsubrn  35722  msubff  35732  msubvrs  35762  mclsssvlem  35764  faclim  35948  curf  37937  uncf  37938  curunc  37941  unccur  37942  matunitlindflem1  37955  matunitlindflem2  37956  ptrecube  37959  heicant  37994  mblfinlem2  37997  itg2addnclem  38010  ftc1anclem1  38032  ftc1anclem2  38033  ftc1anclem4  38035  upixp  38068  fdc  38084  seqpo  38086  incsequz  38087  incsequz2  38088  metf1o  38094  geomcau  38098  sstotbnd2  38113  prdsbnd  38132  ismtyima  38142  ismtyhmeolem  38143  heiborlem3  38152  heiborlem6  38155  heiborlem10  38159  bfplem1  38161  ghomco  38230  sticksstones11  42613  mzpclall  43177  mzprename  43199  rexrabdioph  43244  rmydioph  43464  rmxdioph  43466  expdiophlem2  43472  expdioph  43473  pw2f1ocnv  43487  kelac1  43513  rngunsnply  43619  ofsubid  44773  ofdivrec  44775  ofdivcan4  44776  ofdivdiv2  44777  dvconstbi  44783  refsum2cnlem1  45490  climinf  46058  stoweidlem26  46476  stoweidlem60  46510  stoweid  46513  dmvolsal  46796  caratheodory  46978  elhoi  46992  smfresal  47238  f1oresf1o2  47755  fargshiftf  47916  nnsum4primeseven  48292  nnsum4primesevenALTV  48293  isubgrvtxuhgr  48356  isubgruhgr  48360  isubgr0uhgr  48365  grimuhgr  48379  gricushgr  48409  rmsupp0  48860  domnmsuppn0  48861  gsumlsscl  48872  lincfsuppcl  48905  linccl  48906  lincdifsn  48916  lincsum  48921  lincscm  48922  lincscmcl  48924  lincext1  48946  lindslinindimp2lem1  48950  lindslinindimp2lem4  48953  lindslinindsimp2lem5  48954  snlindsntor  48963  lincresunitlem2  48968  lincresunit3lem1  48971  lincresunit3lem2  48972  lincresunit3  48973  lincreslvec3  48974  isldepslvec2  48977  zlmodzxzldeplem3  48994  1arympt1  49130  ackendofnn0  49176  xpco2  49348  aacllem  50292