Theorem ffvelcdm 7024

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ran crn 5623   Fn wfn 6485  ⟶wf 6486  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498

This theorem is referenced by:  ffvelcdmi  7026  ffvelcdmda  7027  dffo3  7045  dffo3f  7049  foco2  7052  ffnfv  7062  ffvresb  7068  fcompt  7076  fsn2  7079  fvconst  7106  fprb  7138  f1cofveqaeq  7201  fcofo  7232  cocan1  7235  fvf1pr  7251  isocnv  7274  isocnv3  7276  isores2  7277  isopolem  7289  isosolem  7291  fovcdm  7526  off  7638  fnwelem  8071  soseq  8099  smofvon2  8286  smocdmdom  8298  omsmolem  8583  omsmo  8584  fsetfcdm  8795  mapfvd  8815  mapsncnv  8829  2dom  8965  xpdom2  8998  domunsncan  9003  xpmapenlem  9070  fiint  9225  infdifsn  9564  cantnflem1  9596  wemapwe  9604  cnfcom3lem  9610  updjudhf  9841  fseqenlem1  9932  finacn  9958  ackbij1lem12  10138  cofsmo  10177  cfsmolem  10178  cfcoflem  10180  coftr  10181  isf32lem6  10266  isf32lem7  10267  isf34lem7  10287  isf34lem6  10288  acncc  10348  axdc2lem  10356  axdc3lem2  10359  axdc3lem4  10361  axdc4lem  10363  axcclem  10365  ttukeylem6  10422  alephreg  10491  pwcfsdom  10492  canthp1lem2  10562  canthp1  10563  pwfseqlem1  10567  pwfseqlem4a  10570  gruf  10720  fsequb2  13897  axdc4uzlem  13904  seqf1o  13964  hashf1lem1  14376  wwlktovf  14877  shftf  15000  limsupgre  15402  rlimuni  15471  lo1resb  15485  o1resb  15487  o1of2  15534  o1rlimmul  15540  isercolllem1  15586  isercolllem2  15587  isercolllem3  15588  isercoll  15589  climsup  15591  iseralt  15606  sumeq2ii  15614  summolem2a  15636  isumcl  15682  isumshft  15760  climcndslem2  15771  climcnds  15772  mertenslem2  15806  prodeq2ii  15832  prodmolem2a  15855  iprodcl  15922  rpnnen2lem10  16146  ruclem8  16160  ruclem12  16164  3dvds  16256  smueqlem  16415  nn0seqcvgd  16495  algrf  16498  eucalg  16512  phimullem  16704  pcmpt  16818  pcprod  16821  vdwlem11  16917  vdwnnlem3  16923  ramlb  16945  0ram  16946  ramcl  16955  prmgaplem8  16984  imasaddfnlem  17447  imasaddflem  17449  chnpof1  18551  mgmhmpropd  18621  mhmpropd  18715  smndex1gid  18826  ghmsub  19151  cntzmhm  19268  f1omvdconj  19373  pj1ghm  19630  gsumzaddlem  19848  gsumzadd  19849  gsummptnn0fzfv  19914  dprdfadd  19949  subgdmdprd  19963  gsumdixp  20252  lspcl  20925  znunit  21516  frlmsslsp  21749  frlmup2  21752  lindfmm  21780  islindf4  21791  psrbaglesupp  21876  psrbaglefi  21880  resspsrmul  21929  evlslem4  22029  evlslem3  22033  fvcoe1  22146  psropprmul  22176  00ply1bas  22178  subrgvr1cl  22202  coe1mul2lem1  22207  coe1tmmul  22217  ply1coe  22240  evl1val  22271  evl1sca  22276  pf1const  22288  1mavmul  22490  mavmulass  22491  marepvcl  22511  1marepvmarrepid  22517  cramerimplem1  22625  pmatcollpw3fi1lem1  22728  pmatcollpw3fi1lem2  22729  cpmadugsumlemF  22818  cpmadugsumfi  22819  cayleyhamilton1  22834  hauscmplem  23348  ptbasid  23517  ptpjcn  23553  upxp  23565  uptx  23567  txcmplem2  23584  xkopt  23597  txhmeo  23745  alexsubALTlem3  23991  nrginvrcn  24634  nmoi  24670  nmoleub  24673  cncfmet  24856  cnheibor  24908  evth  24912  pcopt  24976  pcopt2  24977  pcorevlem  24980  pi1xfrf  25007  pi1xfr  25009  pi1xfrcnvlem  25010  iscauf  25234  iscmet3lem1  25245  iscmet3lem2  25246  iscmet3  25247  causs  25252  bcthlem5  25282  bcth3  25285  ovolfcl  25421  ovolfioo  25422  ovolficc  25423  ovolficcss  25424  ovolfsval  25425  ovolmge0  25432  ovollb2lem  25443  ovolunlem1a  25451  ovoliunlem1  25457  ovoliunlem2  25458  ovoliun  25460  ovolicc1  25471  ovolicc2lem3  25474  ovolicc2lem4  25475  ovolicc2lem5  25476  voliunlem1  25505  volsup  25511  ioombl1lem2  25514  ovolfs2  25526  uniioovol  25534  uniiccvol  25535  uniioombllem3a  25539  uniioombllem3  25540  uniioombllem4  25541  uniioombllem5  25542  uniioombllem6  25543  dyadmbl  25555  volcn  25561  ismbf  25583  mbfadd  25616  mbfsub  25617  mbflimsup  25621  0plef  25627  itg1climres  25669  mbfi1fseqlem1  25670  mbfi1fseqlem3  25672  mbfi1fseqlem4  25673  mbfi1fseqlem5  25674  mbfmul  25681  xrge0f  25686  itg2ge0  25690  itg2seq  25697  itg2uba  25698  itg2lea  25699  itg2eqa  25700  itg2splitlem  25703  itg2split  25704  itg2i1fseqle  25709  itg2i1fseq  25710  itg2i1fseq2  25711  itg2addlem  25713  bddmulibl  25794  ellimc3  25834  dvaddbr  25894  dvcobr  25903  dvcobrOLD  25904  dvcj  25908  dvfre  25909  dvcnvlem  25934  dvlip  25952  dvlipcn  25953  c1lip1  25956  tdeglem4  26019  tdeglem2  26020  coe1mul3  26058  ply1rem  26125  fta1g  26129  ig1pdvds  26139  plyf  26157  plyeq0lem  26169  plypf1  26171  plyaddlem  26174  plymullem  26175  plyco  26200  dgreq  26203  0dgrb  26205  coefv0  26207  coeaddlem  26208  coemullem  26209  coemulc  26214  plycn  26220  plycnOLD  26221  dgrcolem2  26234  plycjlem  26236  plycj  26237  plycjOLD  26239  plyrecj  26241  plyreres  26244  dvply1  26245  vieta1lem2  26273  vieta1  26274  elqaalem2  26282  aareccl  26288  aalioulem1  26294  ulmcaulem  26357  ulmcau  26358  ulmcn  26362  mtest  26367  psergf  26375  dvradcnv  26384  psercn2  26386  psercn2OLD  26387  pserdvlem2  26392  pserdv2  26394  abelthlem6  26400  abelthlem8  26403  abelthlem9  26404  logtayl  26623  amgm  26955  ftalem1  27037  ftalem2  27038  ftalem3  27039  ftalem4  27040  ftalem5  27041  basellem2  27046  muinv  27157  dchrmulcl  27214  dchrinvcl  27218  dchrfi  27220  dchrghm  27221  dchrsum2  27233  dchrsum  27234  bposlem5  27253  lgscllem  27269  lgsval4a  27284  lgsneg  27286  lgsdir  27297  lgsdilem2  27298  lgsdi  27299  lgsne0  27300  lgseisenlem3  27342  rpvmasumlem  27452  dchrmusum2  27459  dchrvmasumiflem1  27466  dchrisum0ff  27472  dchrisum0flblem1  27473  dchrisum0fno1  27476  rpvmasum2  27477  dchrisum0re  27478  dchrisum0lem2a  27482  upgrreslem  29326  umgrreslem  29327  wlkpvtx  29680  wlkepvtx  29681  usgr2pthlem  29785  frgrncvvdeqlem8  30330  lnoadd  30782  lnosub  30783  nmosetre  30788  nmooge0  30791  nmoub3i  30797  nmounbi  30800  phoeqi  30881  ubthlem1  30894  h2hcau  31003  h2hlm  31004  hoscl  31769  homcl  31770  hodcl  31771  hoaddcl  31782  homulcl  31783  homullid  31824  homco1  31825  homulass  31826  hoadddi  31827  hoadddir  31828  hoeq1  31854  hoeq2  31855  adjsym  31857  nmopsetretALT  31887  nmfnsetre  31901  cnvadj  31916  hhcno  31928  hhcnf  31929  nmopub2tALT  31933  nmopge0  31935  unopf1o  31940  unoplin  31944  counop  31945  nmfnleub2  31950  nmfnge0  31951  hmoplin  31966  eigvalcl  31985  lnop0  31990  hmops  32044  hmopm  32045  nlelchi  32085  leop2  32148  leopadd  32156  leopmuli  32157  leopnmid  32162  hmopidmchi  32175  pjinvari  32215  sticl  32239  fcomptf  32685  rge0scvg  34055  esumcst  34169  esumfzf  34175  esumfsup  34176  esumfsupre  34177  hasheuni  34191  measdivcstALTV  34331  eulerpartlems  34466  eulerpartlemgc  34468  eulerpartlemb  34474  derangsn  35313  subfacp1lem5  35327  subfacp1lem6  35328  pconnconn  35374  sconnpi1  35382  txsconnlem  35383  cvxsconn  35386  cvmliftphtlem  35460  cvmlift3lem2  35463  cvmlift3lem4  35465  cvmlift3lem6  35467  satfvel  35555  satefvfmla1  35568  elmrsubrn  35663  msubff  35673  msubvrs  35703  mclsssvlem  35705  faclim  35889  curf  37738  uncf  37739  curunc  37742  unccur  37743  matunitlindflem1  37756  matunitlindflem2  37757  ptrecube  37760  heicant  37795  mblfinlem2  37798  itg2addnclem  37811  ftc1anclem1  37833  ftc1anclem2  37834  ftc1anclem4  37836  upixp  37869  fdc  37885  seqpo  37887  incsequz  37888  incsequz2  37889  metf1o  37895  geomcau  37899  sstotbnd2  37914  prdsbnd  37933  ismtyima  37943  ismtyhmeolem  37944  heiborlem3  37953  heiborlem6  37956  heiborlem10  37960  bfplem1  37962  ghomco  38031  sticksstones11  42349  mzpclall  42911  mzprename  42933  rexrabdioph  42978  rmydioph  43198  rmxdioph  43200  expdiophlem2  43206  expdioph  43207  pw2f1ocnv  43221  kelac1  43247  rngunsnply  43353  ofsubid  44507  ofdivrec  44509  ofdivcan4  44510  ofdivdiv2  44511  dvconstbi  44517  refsum2cnlem1  45224  climinf  45794  stoweidlem26  46212  stoweidlem60  46246  stoweid  46249  dmvolsal  46532  caratheodory  46714  elhoi  46728  smfresal  46974  f1oresf1o2  47479  fargshiftf  47628  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  isubgrvtxuhgr  48052  isubgruhgr  48056  isubgr0uhgr  48061  grimuhgr  48075  gricushgr  48105  rmsupp0  48556  domnmsuppn0  48557  gsumlsscl  48568  lincfsuppcl  48601  linccl  48602  lincdifsn  48612  lincsum  48617  lincscm  48618  lincscmcl  48620  lincext1  48642  lindslinindimp2lem1  48646  lindslinindimp2lem4  48649  lindslinindsimp2lem5  48650  snlindsntor  48659  lincresunitlem2  48664  lincresunit3lem1  48667  lincresunit3lem2  48668  lincresunit3  48669  lincreslvec3  48670  isldepslvec2  48673  zlmodzxzldeplem3  48690  1arympt1  48826  ackendofnn0  48872  xpco2  49044  aacllem  49988