Theorem ffvelcdm 7082

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107  ran crn 5668   Fn wfn 6537  ⟶wf 6538  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pr 5414

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-fv 6550

This theorem is referenced by:  ffvelcdmi  7084  ffvelcdmda  7085  dffo3  7103  dffo3f  7107  foco2  7110  ffnfv  7120  ffvresb  7126  fcompt  7134  fsn2  7137  fvconst  7165  fprb  7197  f1cofveqaeq  7261  2f1fvneq  7263  fcofo  7291  cocan1  7294  fvf1pr  7310  isocnv  7333  isocnv3  7335  isores2  7336  isopolem  7348  isosolem  7350  fovcdm  7586  off  7698  fnwelem  8139  soseq  8167  smofvon2  8379  smocdmdom  8391  omsmolem  8678  omsmo  8679  fsetfcdm  8883  mapfvd  8902  mapsncnv  8916  2dom  9053  xpdom2  9090  domunsncan  9095  xpmapenlem  9167  fiint  9349  fiintOLD  9350  infdifsn  9680  cantnflem1  9712  wemapwe  9720  cnfcom3lem  9726  updjudhf  9954  fseqenlem1  10047  finacn  10073  ackbij1lem12  10253  cofsmo  10292  cfsmolem  10293  cfcoflem  10295  coftr  10296  isf32lem6  10381  isf32lem7  10382  isf34lem7  10402  isf34lem6  10403  acncc  10463  axdc2lem  10471  axdc3lem2  10474  axdc3lem4  10476  axdc4lem  10478  axcclem  10480  ttukeylem6  10537  alephreg  10605  pwcfsdom  10606  canthp1lem2  10676  canthp1  10677  pwfseqlem1  10681  pwfseqlem4a  10684  gruf  10834  fsequb2  14000  axdc4uzlem  14007  seqf1o  14067  hashf1lem1  14477  wwlktovf  14978  shftf  15101  limsupgre  15500  rlimuni  15569  lo1resb  15583  o1resb  15585  o1of2  15632  o1rlimmul  15638  isercolllem1  15684  isercolllem2  15685  isercolllem3  15686  isercoll  15687  climsup  15689  iseralt  15704  sumeq2ii  15712  summolem2a  15734  isumcl  15780  isumshft  15858  climcndslem2  15869  climcnds  15870  mertenslem2  15904  prodeq2ii  15930  prodmolem2a  15953  iprodcl  16020  rpnnen2lem10  16242  ruclem8  16256  ruclem12  16260  3dvds  16351  smueqlem  16510  nn0seqcvgd  16590  algrf  16593  eucalg  16607  phimullem  16799  pcmpt  16913  pcprod  16916  vdwlem11  17012  vdwnnlem3  17018  ramlb  17040  0ram  17041  ramcl  17050  prmgaplem8  17079  imasaddfnlem  17549  imasaddflem  17551  mgmhmpropd  18685  mhmpropd  18779  smndex1gid  18890  ghmsub  19216  cntzmhm  19333  f1omvdconj  19437  pj1ghm  19694  gsumzaddlem  19912  gsumzadd  19913  gsummptnn0fzfv  19978  dprdfadd  20013  subgdmdprd  20027  gsumdixp  20289  lspcl  20947  znunit  21549  frlmsslsp  21783  frlmup2  21786  lindfmm  21814  islindf4  21825  psrbaglesupp  21909  psrbaglefi  21913  resspsrmul  21963  evlslem4  22067  evlslem3  22071  fvcoe1  22176  psropprmul  22206  00ply1bas  22208  subrgvr1cl  22232  coe1mul2lem1  22237  coe1tmmul  22247  ply1coe  22269  evl1val  22300  evl1sca  22305  pf1const  22317  1mavmul  22521  mavmulass  22522  marepvcl  22542  1marepvmarrepid  22548  cramerimplem1  22656  pmatcollpw3fi1lem1  22759  pmatcollpw3fi1lem2  22760  cpmadugsumlemF  22849  cpmadugsumfi  22850  cayleyhamilton1  22865  hauscmplem  23379  ptbasid  23548  ptpjcn  23584  upxp  23596  uptx  23598  txcmplem2  23615  xkopt  23628  txhmeo  23776  alexsubALTlem3  24022  nrginvrcn  24668  nmoi  24704  nmoleub  24707  cncfmet  24890  cnheibor  24942  evth  24946  pcopt  25010  pcopt2  25011  pcorevlem  25014  pi1xfrf  25041  pi1xfr  25043  pi1xfrcnvlem  25044  iscauf  25269  iscmet3lem1  25280  iscmet3lem2  25281  iscmet3  25282  causs  25287  bcthlem5  25317  bcth3  25320  ovolfcl  25456  ovolfioo  25457  ovolficc  25458  ovolficcss  25459  ovolfsval  25460  ovolmge0  25467  ovollb2lem  25478  ovolunlem1a  25486  ovoliunlem1  25492  ovoliunlem2  25493  ovoliun  25495  ovolicc1  25506  ovolicc2lem3  25509  ovolicc2lem4  25510  ovolicc2lem5  25511  voliunlem1  25540  volsup  25546  ioombl1lem2  25549  ovolfs2  25561  uniioovol  25569  uniiccvol  25570  uniioombllem3a  25574  uniioombllem3  25575  uniioombllem4  25576  uniioombllem5  25577  uniioombllem6  25578  dyadmbl  25590  volcn  25596  ismbf  25618  mbfadd  25651  mbfsub  25652  mbflimsup  25656  0plef  25662  itg1climres  25704  mbfi1fseqlem1  25705  mbfi1fseqlem3  25707  mbfi1fseqlem4  25708  mbfi1fseqlem5  25709  mbfmul  25716  xrge0f  25721  itg2ge0  25725  itg2seq  25732  itg2uba  25733  itg2lea  25734  itg2eqa  25735  itg2splitlem  25738  itg2split  25739  itg2i1fseqle  25744  itg2i1fseq  25745  itg2i1fseq2  25746  itg2addlem  25748  bddmulibl  25829  ellimc3  25869  dvaddbr  25929  dvcobr  25938  dvcobrOLD  25939  dvcj  25943  dvfre  25944  dvcnvlem  25969  dvlip  25987  dvlipcn  25988  c1lip1  25991  tdeglem4  26054  tdeglem2  26055  coe1mul3  26093  ply1rem  26160  fta1g  26164  ig1pdvds  26174  plyf  26192  plyeq0lem  26204  plypf1  26206  plyaddlem  26209  plymullem  26210  plyco  26235  dgreq  26238  0dgrb  26240  coefv0  26242  coeaddlem  26243  coemullem  26244  coemulc  26249  plycn  26255  plycnOLD  26256  dgrcolem2  26269  plycjlem  26271  plycj  26272  plycjOLD  26274  plyrecj  26276  plyreres  26279  dvply1  26280  vieta1lem2  26308  vieta1  26309  elqaalem2  26317  aareccl  26323  aalioulem1  26329  ulmcaulem  26392  ulmcau  26393  ulmcn  26397  mtest  26402  psergf  26410  dvradcnv  26419  psercn2  26421  psercn2OLD  26422  pserdvlem2  26427  pserdv2  26429  abelthlem6  26435  abelthlem8  26438  abelthlem9  26439  logtayl  26657  amgm  26989  ftalem1  27071  ftalem2  27072  ftalem3  27073  ftalem4  27074  ftalem5  27075  basellem2  27080  muinv  27191  dchrmulcl  27248  dchrinvcl  27252  dchrfi  27254  dchrghm  27255  dchrsum2  27267  dchrsum  27268  bposlem5  27287  lgscllem  27303  lgsval4a  27318  lgsneg  27320  lgsdir  27331  lgsdilem2  27332  lgsdi  27333  lgsne0  27334  lgseisenlem3  27376  rpvmasumlem  27486  dchrmusum2  27493  dchrvmasumiflem1  27500  dchrisum0ff  27506  dchrisum0flblem1  27507  dchrisum0fno1  27510  rpvmasum2  27511  dchrisum0re  27512  dchrisum0lem2a  27516  upgrreslem  29268  umgrreslem  29269  wlkpvtx  29624  wlkepvtx  29625  usgr2pthlem  29730  frgrncvvdeqlem8  30272  lnoadd  30724  lnosub  30725  nmosetre  30730  nmooge0  30733  nmoub3i  30739  nmounbi  30742  phoeqi  30823  ubthlem1  30836  h2hcau  30945  h2hlm  30946  hoscl  31711  homcl  31712  hodcl  31713  hoaddcl  31724  homulcl  31725  homullid  31766  homco1  31767  homulass  31768  hoadddi  31769  hoadddir  31770  hoeq1  31796  hoeq2  31797  adjsym  31799  nmopsetretALT  31829  nmfnsetre  31843  cnvadj  31858  hhcno  31870  hhcnf  31871  nmopub2tALT  31875  nmopge0  31877  unopf1o  31882  unoplin  31886  counop  31887  nmfnleub2  31892  nmfnge0  31893  hmoplin  31908  eigvalcl  31927  lnop0  31932  hmops  31986  hmopm  31987  nlelchi  32027  leop2  32090  leopadd  32098  leopmuli  32099  leopnmid  32104  hmopidmchi  32117  pjinvari  32157  sticl  32181  fcomptf  32615  rge0scvg  33889  esumcst  34005  esumfzf  34011  esumfsup  34012  esumfsupre  34013  hasheuni  34027  measdivcstALTV  34167  eulerpartlems  34303  eulerpartlemgc  34305  eulerpartlemb  34311  derangsn  35116  subfacp1lem5  35130  subfacp1lem6  35131  pconnconn  35177  sconnpi1  35185  txsconnlem  35186  cvxsconn  35189  cvmliftphtlem  35263  cvmlift3lem2  35266  cvmlift3lem4  35268  cvmlift3lem6  35270  satfvel  35358  satefvfmla1  35371  elmrsubrn  35466  msubff  35476  msubvrs  35506  mclsssvlem  35508  faclim  35687  curf  37546  uncf  37547  curunc  37550  unccur  37551  matunitlindflem1  37564  matunitlindflem2  37565  ptrecube  37568  heicant  37603  mblfinlem2  37606  itg2addnclem  37619  ftc1anclem1  37641  ftc1anclem2  37642  ftc1anclem4  37644  upixp  37677  fdc  37693  seqpo  37695  incsequz  37696  incsequz2  37697  metf1o  37703  geomcau  37707  sstotbnd2  37722  prdsbnd  37741  ismtyima  37751  ismtyhmeolem  37752  heiborlem3  37761  heiborlem6  37764  heiborlem10  37768  bfplem1  37770  ghomco  37839  sticksstones11  42098  mzpclall  42683  mzprename  42705  rexrabdioph  42750  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  pw2f1ocnv  42994  kelac1  43020  rngunsnply  43126  ofsubid  44288  ofdivrec  44290  ofdivcan4  44291  ofdivdiv2  44292  dvconstbi  44298  refsum2cnlem1  44987  climinf  45566  stoweidlem26  45986  stoweidlem60  46020  stoweid  46023  dmvolsal  46306  caratheodory  46488  elhoi  46502  smfresal  46748  f1oresf1o2  47249  fargshiftf  47373  nnsum4primeseven  47733  nnsum4primesevenALTV  47734  isubgrvtxuhgr  47796  isubgruhgr  47800  isubgr0uhgr  47805  grimuhgr  47824  gricushgr  47832  rmsupp0  48230  domnmsuppn0  48231  gsumlsscl  48242  lincfsuppcl  48276  linccl  48277  lincdifsn  48287  lincsum  48292  lincscm  48293  lincscmcl  48295  lincext1  48317  lindslinindimp2lem1  48321  lindslinindimp2lem4  48324  lindslinindsimp2lem5  48325  snlindsntor  48334  lincresunitlem2  48339  lincresunit3lem1  48342  lincresunit3lem2  48343  lincresunit3  48344  lincreslvec3  48345  isldepslvec2  48348  zlmodzxzldeplem3  48365  1arympt1  48505  ackendofnn0  48551  aacllem  49316