Theorem ffvelcdm 7083

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ran crn 5677   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is referenced by:  ffvelcdmi  7085  ffvelcdmda  7086  dffo3  7103  dffo3f  7107  foco2  7110  ffnfv  7120  ffvresb  7126  fcompt  7133  fsn2  7136  fvconst  7164  fprb  7197  f1cofveqaeq  7259  2f1fvneq  7261  fcofo  7288  cocan1  7291  isocnv  7329  isocnv3  7331  isores2  7332  isopolem  7344  isosolem  7346  fovcdm  7579  off  7690  fnwelem  8119  soseq  8147  smofvon2  8358  smocdmdom  8370  omsmolem  8658  omsmo  8659  fsetfcdm  8856  mapfvd  8875  mapsncnv  8889  2dom  9032  xpdom2  9069  domunsncan  9074  xpmapenlem  9146  fiint  9326  infdifsn  9654  cantnflem1  9686  wemapwe  9694  cnfcom3lem  9700  updjudhf  9928  fseqenlem1  10021  finacn  10047  ackbij1lem12  10228  cofsmo  10266  cfsmolem  10267  cfcoflem  10269  coftr  10270  isf32lem6  10355  isf32lem7  10356  isf34lem7  10376  isf34lem6  10377  acncc  10437  axdc2lem  10445  axdc3lem2  10448  axdc3lem4  10450  axdc4lem  10452  axcclem  10454  ttukeylem6  10511  alephreg  10579  pwcfsdom  10580  canthp1lem2  10650  canthp1  10651  pwfseqlem1  10655  pwfseqlem4a  10658  gruf  10808  fsequb2  13943  axdc4uzlem  13950  seqf1o  14011  hashf1lem1  14417  hashf1lem1OLD  14418  wwlktovf  14909  shftf  15028  limsupgre  15427  rlimuni  15496  lo1resb  15510  o1resb  15512  o1of2  15559  o1rlimmul  15565  isercolllem1  15613  isercolllem2  15614  isercolllem3  15615  isercoll  15616  climsup  15618  iseralt  15633  sumeq2ii  15641  summolem2a  15663  isumcl  15709  isumshft  15787  climcndslem2  15798  climcnds  15799  mertenslem2  15833  prodeq2ii  15859  prodmolem2a  15880  iprodcl  15947  rpnnen2lem10  16168  ruclem8  16182  ruclem12  16186  3dvds  16276  smueqlem  16433  nn0seqcvgd  16509  algrf  16512  eucalg  16526  phimullem  16714  pcmpt  16827  pcprod  16830  vdwlem11  16926  vdwnnlem3  16932  ramlb  16954  0ram  16955  ramcl  16964  prmgaplem8  16993  imasaddfnlem  17476  imasaddflem  17478  mhmpropd  18680  smndex1gid  18786  ghmsub  19102  cntzmhm  19207  f1omvdconj  19316  pj1ghm  19573  gsumzaddlem  19791  gsumzadd  19792  gsummptnn0fzfv  19857  dprdfadd  19892  subgdmdprd  19906  gsumdixp  20135  lspcl  20592  znunit  21125  frlmsslsp  21357  frlmup2  21360  lindfmm  21388  islindf4  21399  psrbaglesupp  21483  psrbaglesuppOLD  21484  psrbaglefi  21491  psrbaglefiOLD  21492  resspsrmul  21543  evlslem4  21643  evlslem3  21649  fvcoe1  21737  psropprmul  21767  00ply1bas  21769  subrgvr1cl  21791  coe1mul2lem1  21796  coe1tmmul  21806  ply1coe  21827  evl1val  21855  evl1sca  21860  pf1const  21872  1mavmul  22057  mavmulass  22058  marepvcl  22078  1marepvmarrepid  22084  cramerimplem1  22192  pmatcollpw3fi1lem1  22295  pmatcollpw3fi1lem2  22296  cpmadugsumlemF  22385  cpmadugsumfi  22386  cayleyhamilton1  22401  hauscmplem  22917  ptbasid  23086  ptpjcn  23122  upxp  23134  uptx  23136  txcmplem2  23153  xkopt  23166  txhmeo  23314  alexsubALTlem3  23560  nrginvrcn  24216  nmoi  24252  nmoleub  24255  cncfmet  24432  cnheibor  24478  evth  24482  pcopt  24545  pcopt2  24546  pcorevlem  24549  pi1xfrf  24576  pi1xfr  24578  pi1xfrcnvlem  24579  iscauf  24804  iscmet3lem1  24815  iscmet3lem2  24816  iscmet3  24817  causs  24822  bcthlem5  24852  bcth3  24855  ovolfcl  24990  ovolfioo  24991  ovolficc  24992  ovolficcss  24993  ovolfsval  24994  ovolmge0  25001  ovollb2lem  25012  ovolunlem1a  25020  ovoliunlem1  25026  ovoliunlem2  25027  ovoliun  25029  ovolicc1  25040  ovolicc2lem3  25043  ovolicc2lem4  25044  ovolicc2lem5  25045  voliunlem1  25074  volsup  25080  ioombl1lem2  25083  ovolfs2  25095  uniioovol  25103  uniiccvol  25104  uniioombllem3a  25108  uniioombllem3  25109  uniioombllem4  25110  uniioombllem5  25111  uniioombllem6  25112  dyadmbl  25124  volcn  25130  ismbf  25152  mbfadd  25185  mbfsub  25186  mbflimsup  25190  0plef  25196  itg1climres  25239  mbfi1fseqlem1  25240  mbfi1fseqlem3  25242  mbfi1fseqlem4  25243  mbfi1fseqlem5  25244  mbfmul  25251  xrge0f  25256  itg2ge0  25260  itg2seq  25267  itg2uba  25268  itg2lea  25269  itg2eqa  25270  itg2splitlem  25273  itg2split  25274  itg2i1fseqle  25279  itg2i1fseq  25280  itg2i1fseq2  25281  itg2addlem  25283  bddmulibl  25363  ellimc3  25403  dvaddbr  25462  dvcobr  25470  dvcj  25474  dvfre  25475  dvcnvlem  25500  dvlip  25517  dvlipcn  25518  c1lip1  25521  tdeglem4  25584  tdeglem4OLD  25585  tdeglem2  25586  coe1mul3  25624  ply1rem  25688  fta1g  25692  ig1pdvds  25701  plyf  25719  plyeq0lem  25731  plypf1  25733  plyaddlem  25736  plymullem  25737  plyco  25762  dgreq  25765  0dgrb  25767  coefv0  25769  coeaddlem  25770  coemullem  25771  coemulc  25776  plycn  25782  dgrcolem2  25795  plycjlem  25797  plycj  25798  plyrecj  25800  plyreres  25803  dvply1  25804  vieta1lem2  25831  vieta1  25832  elqaalem2  25840  aareccl  25846  aalioulem1  25852  ulmcaulem  25913  ulmcau  25914  ulmcn  25918  mtest  25923  psergf  25931  dvradcnv  25940  psercn2  25942  pserdvlem2  25947  pserdv2  25949  abelthlem6  25955  abelthlem8  25958  abelthlem9  25959  logtayl  26175  amgm  26502  ftalem1  26584  ftalem2  26585  ftalem3  26586  ftalem4  26587  ftalem5  26588  basellem2  26593  muinv  26704  dchrmulcl  26759  dchrinvcl  26763  dchrfi  26765  dchrghm  26766  dchrsum2  26778  dchrsum  26779  bposlem5  26798  lgscllem  26814  lgsval4a  26829  lgsneg  26831  lgsdir  26842  lgsdilem2  26843  lgsdi  26844  lgsne0  26845  lgseisenlem3  26887  rpvmasumlem  26997  dchrmusum2  27004  dchrvmasumiflem1  27011  dchrisum0ff  27017  dchrisum0flblem1  27018  dchrisum0fno1  27021  rpvmasum2  27022  dchrisum0re  27023  dchrisum0lem2a  27027  upgrreslem  28599  umgrreslem  28600  wlkpvtx  28954  wlkepvtx  28955  usgr2pthlem  29058  frgrncvvdeqlem8  29597  lnoadd  30049  lnosub  30050  nmosetre  30055  nmooge0  30058  nmoub3i  30064  nmounbi  30067  phoeqi  30148  ubthlem1  30161  h2hcau  30270  h2hlm  30271  hoscl  31036  homcl  31037  hodcl  31038  hoaddcl  31049  homulcl  31050  homullid  31091  homco1  31092  homulass  31093  hoadddi  31094  hoadddir  31095  hoeq1  31121  hoeq2  31122  adjsym  31124  nmopsetretALT  31154  nmfnsetre  31168  cnvadj  31183  hhcno  31195  hhcnf  31196  nmopub2tALT  31200  nmopge0  31202  unopf1o  31207  unoplin  31211  counop  31212  nmfnleub2  31217  nmfnge0  31218  hmoplin  31233  eigvalcl  31252  lnop0  31257  hmops  31311  hmopm  31312  nlelchi  31352  leop2  31415  leopadd  31423  leopmuli  31424  leopnmid  31429  hmopidmchi  31442  pjinvari  31482  sticl  31506  fcomptf  31921  rge0scvg  32998  esumcst  33130  esumfzf  33136  esumfsup  33137  esumfsupre  33138  hasheuni  33152  measdivcstALTV  33292  eulerpartlems  33428  eulerpartlemgc  33430  eulerpartlemb  33436  derangsn  34230  subfacp1lem5  34244  subfacp1lem6  34245  pconnconn  34291  sconnpi1  34299  txsconnlem  34300  cvxsconn  34303  cvmliftphtlem  34377  cvmlift3lem2  34380  cvmlift3lem4  34382  cvmlift3lem6  34384  satfvel  34472  satefvfmla1  34485  elmrsubrn  34580  msubff  34590  msubvrs  34620  mclsssvlem  34622  faclim  34785  gg-dvcobr  35245  gg-plycn  35246  gg-psercn2  35247  curf  36552  uncf  36553  curunc  36556  unccur  36557  matunitlindflem1  36570  matunitlindflem2  36571  ptrecube  36574  heicant  36609  mblfinlem2  36612  itg2addnclem  36625  ftc1anclem1  36647  ftc1anclem2  36648  ftc1anclem4  36650  upixp  36683  fdc  36699  seqpo  36701  incsequz  36702  incsequz2  36703  metf1o  36709  geomcau  36713  sstotbnd2  36728  prdsbnd  36747  ismtyima  36757  ismtyhmeolem  36758  heiborlem3  36767  heiborlem6  36770  heiborlem10  36774  bfplem1  36776  ghomco  36845  sticksstones11  41058  mzpclall  41547  mzprename  41569  rexrabdioph  41614  rmydioph  41835  rmxdioph  41837  expdiophlem2  41843  expdioph  41844  pw2f1ocnv  41858  kelac1  41887  rngunsnply  41997  ofsubid  43165  ofdivrec  43167  ofdivcan4  43168  ofdivdiv2  43169  dvconstbi  43175  refsum2cnlem1  43803  climinf  44401  stoweidlem26  44821  stoweidlem60  44855  stoweid  44858  dmvolsal  45141  caratheodory  45323  elhoi  45337  smfresal  45583  f1oresf1o2  46078  fargshiftf  46187  nnsum4primeseven  46547  nnsum4primesevenALTV  46548  isomushgr  46573  isomgrtrlem  46585  mgmhmpropd  46634  rmsupp0  47123  domnmsuppn0  47124  gsumlsscl  47138  lincfsuppcl  47172  linccl  47173  lincdifsn  47183  lincsum  47188  lincscm  47189  lincscmcl  47191  lincext1  47213  lindslinindimp2lem1  47217  lindslinindimp2lem4  47220  lindslinindsimp2lem5  47221  snlindsntor  47230  lincresunitlem2  47235  lincresunit3lem1  47238  lincresunit3lem2  47239  lincresunit3  47240  lincreslvec3  47241  isldepslvec2  47244  zlmodzxzldeplem3  47261  1arympt1  47402  ackendofnn0  47448  aacllem  47926