Theorem ffvelcdm 7037

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 6672	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7036	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 581	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6679	. . . 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 2114  ran crn 5635   Fn wfn 6497  ⟶wf 6498  ‘cfv 6502

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 5245  ax-nul 5255  ax-pr 5381

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510

This theorem is referenced by:  ffvelcdmi  7039  ffvelcdmda  7040  dffo3  7058  dffo3f  7062  foco2  7065  ffnfv  7075  ffvresb  7082  fcompt  7090  fsn2  7093  fvconst  7120  fprb  7152  f1cofveqaeq  7215  fcofo  7246  cocan1  7249  fvf1pr  7265  isocnv  7288  isocnv3  7290  isores2  7291  isopolem  7303  isosolem  7305  fovcdm  7540  off  7652  fnwelem  8085  soseq  8113  smofvon2  8300  smocdmdom  8312  omsmolem  8597  omsmo  8598  fsetfcdm  8811  mapfvd  8831  mapsncnv  8845  2dom  8981  xpdom2  9014  domunsncan  9019  xpmapenlem  9086  fiint  9241  infdifsn  9580  cantnflem1  9612  wemapwe  9620  cnfcom3lem  9626  updjudhf  9857  fseqenlem1  9948  finacn  9974  ackbij1lem12  10154  cofsmo  10193  cfsmolem  10194  cfcoflem  10196  coftr  10197  isf32lem6  10282  isf32lem7  10283  isf34lem7  10303  isf34lem6  10304  acncc  10364  axdc2lem  10372  axdc3lem2  10375  axdc3lem4  10377  axdc4lem  10379  axcclem  10381  ttukeylem6  10438  alephreg  10507  pwcfsdom  10508  canthp1lem2  10578  canthp1  10579  pwfseqlem1  10583  pwfseqlem4a  10586  gruf  10736  fsequb2  13913  axdc4uzlem  13920  seqf1o  13980  hashf1lem1  14392  wwlktovf  14893  shftf  15016  limsupgre  15418  rlimuni  15487  lo1resb  15501  o1resb  15503  o1of2  15550  o1rlimmul  15556  isercolllem1  15602  isercolllem2  15603  isercolllem3  15604  isercoll  15605  climsup  15607  iseralt  15622  sumeq2ii  15630  summolem2a  15652  isumcl  15698  isumshft  15776  climcndslem2  15787  climcnds  15788  mertenslem2  15822  prodeq2ii  15848  prodmolem2a  15871  iprodcl  15938  rpnnen2lem10  16162  ruclem8  16176  ruclem12  16180  3dvds  16272  smueqlem  16431  nn0seqcvgd  16511  algrf  16514  eucalg  16528  phimullem  16720  pcmpt  16834  pcprod  16837  vdwlem11  16933  vdwnnlem3  16939  ramlb  16961  0ram  16962  ramcl  16971  prmgaplem8  17000  imasaddfnlem  17463  imasaddflem  17465  chnpof1  18567  mgmhmpropd  18637  mhmpropd  18731  smndex1gid  18843  smndex1gidOLD  18844  ghmsub  19170  cntzmhm  19287  f1omvdconj  19392  pj1ghm  19649  gsumzaddlem  19867  gsumzadd  19868  gsummptnn0fzfv  19933  dprdfadd  19968  subgdmdprd  19982  gsumdixp  20271  lspcl  20944  znunit  21535  frlmsslsp  21768  frlmup2  21771  lindfmm  21799  islindf4  21810  psrbaglesupp  21895  psrbaglefi  21899  resspsrmul  21948  evlslem4  22048  evlslem3  22052  fvcoe1  22165  psropprmul  22195  00ply1bas  22197  subrgvr1cl  22221  coe1mul2lem1  22226  coe1tmmul  22236  ply1coe  22259  evl1val  22290  evl1sca  22295  pf1const  22307  1mavmul  22509  mavmulass  22510  marepvcl  22530  1marepvmarrepid  22536  cramerimplem1  22644  pmatcollpw3fi1lem1  22747  pmatcollpw3fi1lem2  22748  cpmadugsumlemF  22837  cpmadugsumfi  22838  cayleyhamilton1  22853  hauscmplem  23367  ptbasid  23536  ptpjcn  23572  upxp  23584  uptx  23586  txcmplem2  23603  xkopt  23616  txhmeo  23764  alexsubALTlem3  24010  nrginvrcn  24653  nmoi  24689  nmoleub  24692  cncfmet  24875  cnheibor  24927  evth  24931  pcopt  24995  pcopt2  24996  pcorevlem  24999  pi1xfrf  25026  pi1xfr  25028  pi1xfrcnvlem  25029  iscauf  25253  iscmet3lem1  25264  iscmet3lem2  25265  iscmet3  25266  causs  25271  bcthlem5  25301  bcth3  25304  ovolfcl  25440  ovolfioo  25441  ovolficc  25442  ovolficcss  25443  ovolfsval  25444  ovolmge0  25451  ovollb2lem  25462  ovolunlem1a  25470  ovoliunlem1  25476  ovoliunlem2  25477  ovoliun  25479  ovolicc1  25490  ovolicc2lem3  25493  ovolicc2lem4  25494  ovolicc2lem5  25495  voliunlem1  25524  volsup  25530  ioombl1lem2  25533  ovolfs2  25545  uniioovol  25553  uniiccvol  25554  uniioombllem3a  25558  uniioombllem3  25559  uniioombllem4  25560  uniioombllem5  25561  uniioombllem6  25562  dyadmbl  25574  volcn  25580  ismbf  25602  mbfadd  25635  mbfsub  25636  mbflimsup  25640  0plef  25646  itg1climres  25688  mbfi1fseqlem1  25689  mbfi1fseqlem3  25691  mbfi1fseqlem4  25692  mbfi1fseqlem5  25693  mbfmul  25700  xrge0f  25705  itg2ge0  25709  itg2seq  25716  itg2uba  25717  itg2lea  25718  itg2eqa  25719  itg2splitlem  25722  itg2split  25723  itg2i1fseqle  25728  itg2i1fseq  25729  itg2i1fseq2  25730  itg2addlem  25732  bddmulibl  25813  ellimc3  25853  dvaddbr  25913  dvcobr  25922  dvcobrOLD  25923  dvcj  25927  dvfre  25928  dvcnvlem  25953  dvlip  25971  dvlipcn  25972  c1lip1  25975  tdeglem4  26038  tdeglem2  26039  coe1mul3  26077  ply1rem  26144  fta1g  26148  ig1pdvds  26158  plyf  26176  plyeq0lem  26188  plypf1  26190  plyaddlem  26193  plymullem  26194  plyco  26219  dgreq  26222  0dgrb  26224  coefv0  26226  coeaddlem  26227  coemullem  26228  coemulc  26233  plycn  26239  plycnOLD  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  psercn2OLD  26406  pserdvlem2  26411  pserdv2  26413  abelthlem6  26419  abelthlem8  26422  abelthlem9  26423  logtayl  26642  amgm  26974  ftalem1  27056  ftalem2  27057  ftalem3  27058  ftalem4  27059  ftalem5  27060  basellem2  27065  muinv  27176  dchrmulcl  27233  dchrinvcl  27237  dchrfi  27239  dchrghm  27240  dchrsum2  27252  dchrsum  27253  bposlem5  27272  lgscllem  27288  lgsval4a  27303  lgsneg  27305  lgsdir  27316  lgsdilem2  27317  lgsdi  27318  lgsne0  27319  lgseisenlem3  27361  rpvmasumlem  27471  dchrmusum2  27478  dchrvmasumiflem1  27485  dchrisum0ff  27491  dchrisum0flblem1  27492  dchrisum0fno1  27495  rpvmasum2  27496  dchrisum0re  27497  dchrisum0lem2a  27501  upgrreslem  29395  umgrreslem  29396  wlkpvtx  29749  wlkepvtx  29750  usgr2pthlem  29854  frgrncvvdeqlem8  30399  lnoadd  30852  lnosub  30853  nmosetre  30858  nmooge0  30861  nmoub3i  30867  nmounbi  30870  phoeqi  30951  ubthlem1  30964  h2hcau  31073  h2hlm  31074  hoscl  31839  homcl  31840  hodcl  31841  hoaddcl  31852  homulcl  31853  homullid  31894  homco1  31895  homulass  31896  hoadddi  31897  hoadddir  31898  hoeq1  31924  hoeq2  31925  adjsym  31927  nmopsetretALT  31957  nmfnsetre  31971  cnvadj  31986  hhcno  31998  hhcnf  31999  nmopub2tALT  32003  nmopge0  32005  unopf1o  32010  unoplin  32014  counop  32015  nmfnleub2  32020  nmfnge0  32021  hmoplin  32036  eigvalcl  32055  lnop0  32060  hmops  32114  hmopm  32115  nlelchi  32155  leop2  32218  leopadd  32226  leopmuli  32227  leopnmid  32232  hmopidmchi  32245  pjinvari  32285  sticl  32309  fcomptf  32754  rge0scvg  34133  esumcst  34247  esumfzf  34253  esumfsup  34254  esumfsupre  34255  hasheuni  34269  measdivcstALTV  34409  eulerpartlems  34544  eulerpartlemgc  34546  eulerpartlemb  34552  derangsn  35392  subfacp1lem5  35406  subfacp1lem6  35407  pconnconn  35453  sconnpi1  35461  txsconnlem  35462  cvxsconn  35465  cvmliftphtlem  35539  cvmlift3lem2  35542  cvmlift3lem4  35544  cvmlift3lem6  35546  satfvel  35634  satefvfmla1  35647  elmrsubrn  35742  msubff  35752  msubvrs  35782  mclsssvlem  35784  faclim  35968  curf  37878  uncf  37879  curunc  37882  unccur  37883  matunitlindflem1  37896  matunitlindflem2  37897  ptrecube  37900  heicant  37935  mblfinlem2  37938  itg2addnclem  37951  ftc1anclem1  37973  ftc1anclem2  37974  ftc1anclem4  37976  upixp  38009  fdc  38025  seqpo  38027  incsequz  38028  incsequz2  38029  metf1o  38035  geomcau  38039  sstotbnd2  38054  prdsbnd  38073  ismtyima  38083  ismtyhmeolem  38084  heiborlem3  38093  heiborlem6  38096  heiborlem10  38100  bfplem1  38102  ghomco  38171  sticksstones11  42555  mzpclall  43113  mzprename  43135  rexrabdioph  43180  rmydioph  43400  rmxdioph  43402  expdiophlem2  43408  expdioph  43409  pw2f1ocnv  43423  kelac1  43449  rngunsnply  43555  ofsubid  44709  ofdivrec  44711  ofdivcan4  44712  ofdivdiv2  44713  dvconstbi  44719  refsum2cnlem1  45426  climinf  45995  stoweidlem26  46413  stoweidlem60  46447  stoweid  46450  dmvolsal  46733  caratheodory  46915  elhoi  46929  smfresal  47175  f1oresf1o2  47680  fargshiftf  47829  nnsum4primeseven  48189  nnsum4primesevenALTV  48190  isubgrvtxuhgr  48253  isubgruhgr  48257  isubgr0uhgr  48262  grimuhgr  48276  gricushgr  48306  rmsupp0  48757  domnmsuppn0  48758  gsumlsscl  48769  lincfsuppcl  48802  linccl  48803  lincdifsn  48813  lincsum  48818  lincscm  48819  lincscmcl  48821  lincext1  48843  lindslinindimp2lem1  48847  lindslinindimp2lem4  48850  lindslinindsimp2lem5  48851  snlindsntor  48860  lincresunitlem2  48865  lincresunit3lem1  48868  lincresunit3lem2  48869  lincresunit3  48870  lincreslvec3  48871  isldepslvec2  48874  zlmodzxzldeplem3  48891  1arympt1  49027  ackendofnn0  49073  xpco2  49245  aacllem  50189