Theorem ffvelcdm 7032

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ran crn 5634   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496

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 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384

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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504

This theorem is referenced by:  ffvelcdmi  7034  ffvelcdmda  7035  dffo3  7052  foco2  7057  ffnfv  7066  ffvresb  7072  fcompt  7079  fsn2  7082  fvconst  7110  fprb  7143  f1cofveqaeq  7205  2f1fvneq  7207  fcofo  7234  cocan1  7237  isocnv  7275  isocnv3  7277  isores2  7278  isopolem  7290  isosolem  7292  fovcdm  7524  off  7635  fnwelem  8063  soseq  8091  smofvon2  8302  smocdmdom  8314  omsmolem  8603  omsmo  8604  fsetfcdm  8798  mapfvd  8817  mapsncnv  8831  2dom  8974  xpdom2  9011  domunsncan  9016  xpmapenlem  9088  fiint  9268  infdifsn  9593  cantnflem1  9625  wemapwe  9633  cnfcom3lem  9639  updjudhf  9867  fseqenlem1  9960  finacn  9986  ackbij1lem12  10167  cofsmo  10205  cfsmolem  10206  cfcoflem  10208  coftr  10209  isf32lem6  10294  isf32lem7  10295  isf34lem7  10315  isf34lem6  10316  acncc  10376  axdc2lem  10384  axdc3lem2  10387  axdc3lem4  10389  axdc4lem  10391  axcclem  10393  ttukeylem6  10450  alephreg  10518  pwcfsdom  10519  canthp1lem2  10589  canthp1  10590  pwfseqlem1  10594  pwfseqlem4a  10597  gruf  10747  fsequb2  13881  axdc4uzlem  13888  seqf1o  13949  hashf1lem1  14353  hashf1lem1OLD  14354  wwlktovf  14845  shftf  14964  limsupgre  15363  rlimuni  15432  lo1resb  15446  o1resb  15448  o1of2  15495  o1rlimmul  15501  isercolllem1  15549  isercolllem2  15550  isercolllem3  15551  isercoll  15552  climsup  15554  iseralt  15569  sumeq2ii  15578  summolem2a  15600  isumcl  15646  isumshft  15724  climcndslem2  15735  climcnds  15736  mertenslem2  15770  prodeq2ii  15796  prodmolem2a  15817  iprodcl  15884  rpnnen2lem10  16105  ruclem8  16119  ruclem12  16123  3dvds  16213  smueqlem  16370  nn0seqcvgd  16446  algrf  16449  eucalg  16463  phimullem  16651  pcmpt  16764  pcprod  16767  vdwlem11  16863  vdwnnlem3  16869  ramlb  16891  0ram  16892  ramcl  16901  prmgaplem8  16930  imasaddfnlem  17410  imasaddflem  17412  mhmpropd  18608  smndex1gid  18713  ghmsub  19016  cntzmhm  19119  f1omvdconj  19228  pj1ghm  19485  gsumzaddlem  19698  gsumzadd  19699  gsummptnn0fzfv  19764  dprdfadd  19799  subgdmdprd  19813  gsumdixp  20033  lspcl  20437  znunit  20970  frlmsslsp  21202  frlmup2  21205  lindfmm  21233  islindf4  21244  psrbaglesupp  21326  psrbaglesuppOLD  21327  psrbaglefi  21334  psrbaglefiOLD  21335  resspsrmul  21386  evlslem4  21484  evlslem3  21490  fvcoe1  21578  psropprmul  21609  00ply1bas  21611  subrgvr1cl  21633  coe1mul2lem1  21638  coe1tmmul  21648  ply1coe  21667  evl1val  21695  evl1sca  21700  pf1const  21712  1mavmul  21897  mavmulass  21898  marepvcl  21918  1marepvmarrepid  21924  cramerimplem1  22032  pmatcollpw3fi1lem1  22135  pmatcollpw3fi1lem2  22136  cpmadugsumlemF  22225  cpmadugsumfi  22226  cayleyhamilton1  22241  hauscmplem  22757  ptbasid  22926  ptpjcn  22962  upxp  22974  uptx  22976  txcmplem2  22993  xkopt  23006  txhmeo  23154  alexsubALTlem3  23400  nrginvrcn  24056  nmoi  24092  nmoleub  24095  cncfmet  24272  cnheibor  24318  evth  24322  pcopt  24385  pcopt2  24386  pcorevlem  24389  pi1xfrf  24416  pi1xfr  24418  pi1xfrcnvlem  24419  iscauf  24644  iscmet3lem1  24655  iscmet3lem2  24656  iscmet3  24657  causs  24662  bcthlem5  24692  bcth3  24695  ovolfcl  24830  ovolfioo  24831  ovolficc  24832  ovolficcss  24833  ovolfsval  24834  ovolmge0  24841  ovollb2lem  24852  ovolunlem1a  24860  ovoliunlem1  24866  ovoliunlem2  24867  ovoliun  24869  ovolicc1  24880  ovolicc2lem3  24883  ovolicc2lem4  24884  ovolicc2lem5  24885  voliunlem1  24914  volsup  24920  ioombl1lem2  24923  ovolfs2  24935  uniioovol  24943  uniiccvol  24944  uniioombllem3a  24948  uniioombllem3  24949  uniioombllem4  24950  uniioombllem5  24951  uniioombllem6  24952  dyadmbl  24964  volcn  24970  ismbf  24992  mbfadd  25025  mbfsub  25026  mbflimsup  25030  0plef  25036  itg1climres  25079  mbfi1fseqlem1  25080  mbfi1fseqlem3  25082  mbfi1fseqlem4  25083  mbfi1fseqlem5  25084  mbfmul  25091  xrge0f  25096  itg2ge0  25100  itg2seq  25107  itg2uba  25108  itg2lea  25109  itg2eqa  25110  itg2splitlem  25113  itg2split  25114  itg2i1fseqle  25119  itg2i1fseq  25120  itg2i1fseq2  25121  itg2addlem  25123  bddmulibl  25203  ellimc3  25243  dvaddbr  25302  dvcobr  25310  dvcj  25314  dvfre  25315  dvcnvlem  25340  dvlip  25357  dvlipcn  25358  c1lip1  25361  tdeglem4  25424  tdeglem4OLD  25425  tdeglem2  25426  coe1mul3  25464  ply1rem  25528  fta1g  25532  ig1pdvds  25541  plyf  25559  plyeq0lem  25571  plypf1  25573  plyaddlem  25576  plymullem  25577  plyco  25602  dgreq  25605  0dgrb  25607  coefv0  25609  coeaddlem  25610  coemullem  25611  coemulc  25616  plycn  25622  dgrcolem2  25635  plycjlem  25637  plycj  25638  plyrecj  25640  plyreres  25643  dvply1  25644  vieta1lem2  25671  vieta1  25672  elqaalem2  25680  aareccl  25686  aalioulem1  25692  ulmcaulem  25753  ulmcau  25754  ulmcn  25758  mtest  25763  psergf  25771  dvradcnv  25780  psercn2  25782  pserdvlem2  25787  pserdv2  25789  abelthlem6  25795  abelthlem8  25798  abelthlem9  25799  logtayl  26015  amgm  26340  ftalem1  26422  ftalem2  26423  ftalem3  26424  ftalem4  26425  ftalem5  26426  basellem2  26431  muinv  26542  dchrmulcl  26597  dchrinvcl  26601  dchrfi  26603  dchrghm  26604  dchrsum2  26616  dchrsum  26617  bposlem5  26636  lgscllem  26652  lgsval4a  26667  lgsneg  26669  lgsdir  26680  lgsdilem2  26681  lgsdi  26682  lgsne0  26683  lgseisenlem3  26725  rpvmasumlem  26835  dchrmusum2  26842  dchrvmasumiflem1  26849  dchrisum0ff  26855  dchrisum0flblem1  26856  dchrisum0fno1  26859  rpvmasum2  26860  dchrisum0re  26861  dchrisum0lem2a  26865  upgrreslem  28252  umgrreslem  28253  wlkpvtx  28607  wlkepvtx  28608  usgr2pthlem  28711  frgrncvvdeqlem8  29250  lnoadd  29700  lnosub  29701  nmosetre  29706  nmooge0  29709  nmoub3i  29715  nmounbi  29718  phoeqi  29799  ubthlem1  29812  h2hcau  29921  h2hlm  29922  hoscl  30687  homcl  30688  hodcl  30689  hoaddcl  30700  homulcl  30701  homulid2  30742  homco1  30743  homulass  30744  hoadddi  30745  hoadddir  30746  hoeq1  30772  hoeq2  30773  adjsym  30775  nmopsetretALT  30805  nmfnsetre  30819  cnvadj  30834  hhcno  30846  hhcnf  30847  nmopub2tALT  30851  nmopge0  30853  unopf1o  30858  unoplin  30862  counop  30863  nmfnleub2  30868  nmfnge0  30869  hmoplin  30884  eigvalcl  30903  lnop0  30908  hmops  30962  hmopm  30963  nlelchi  31003  leop2  31066  leopadd  31074  leopmuli  31075  leopnmid  31080  hmopidmchi  31093  pjinvari  31133  sticl  31157  fcomptf  31574  rge0scvg  32530  esumcst  32662  esumfzf  32668  esumfsup  32669  esumfsupre  32670  hasheuni  32684  measdivcstALTV  32824  eulerpartlems  32960  eulerpartlemgc  32962  eulerpartlemb  32968  derangsn  33764  subfacp1lem5  33778  subfacp1lem6  33779  pconnconn  33825  sconnpi1  33833  txsconnlem  33834  cvxsconn  33837  cvmliftphtlem  33911  cvmlift3lem2  33914  cvmlift3lem4  33916  cvmlift3lem6  33918  satfvel  34006  satefvfmla1  34019  elmrsubrn  34114  msubff  34124  msubvrs  34154  mclsssvlem  34156  faclim  34319  curf  36056  uncf  36057  curunc  36060  unccur  36061  matunitlindflem1  36074  matunitlindflem2  36075  ptrecube  36078  heicant  36113  mblfinlem2  36116  itg2addnclem  36129  ftc1anclem1  36151  ftc1anclem2  36152  ftc1anclem4  36154  upixp  36188  fdc  36204  seqpo  36206  incsequz  36207  incsequz2  36208  metf1o  36214  geomcau  36218  sstotbnd2  36233  prdsbnd  36252  ismtyima  36262  ismtyhmeolem  36263  heiborlem3  36272  heiborlem6  36275  heiborlem10  36279  bfplem1  36281  ghomco  36350  sticksstones11  40564  mzpclall  41036  mzprename  41058  rexrabdioph  41103  rmydioph  41324  rmxdioph  41326  expdiophlem2  41332  expdioph  41333  pw2f1ocnv  41347  kelac1  41376  rngunsnply  41486  ofsubid  42594  ofdivrec  42596  ofdivcan4  42597  ofdivdiv2  42598  dvconstbi  42604  refsum2cnlem1  43232  dffo3f  43388  climinf  43837  stoweidlem26  44257  stoweidlem60  44291  stoweid  44294  dmvolsal  44577  caratheodory  44759  elhoi  44773  smfresal  45019  f1oresf1o2  45513  fargshiftf  45622  nnsum4primeseven  45982  nnsum4primesevenALTV  45983  isomushgr  46008  isomgrtrlem  46020  mgmhmpropd  46069  rmsupp0  46434  domnmsuppn0  46435  gsumlsscl  46449  lincfsuppcl  46484  linccl  46485  lincdifsn  46495  lincsum  46500  lincscm  46501  lincscmcl  46503  lincext1  46525  lindslinindimp2lem1  46529  lindslinindimp2lem4  46532  lindslinindsimp2lem5  46533  snlindsntor  46542  lincresunitlem2  46547  lincresunit3lem1  46550  lincresunit3lem2  46551  lincresunit3  46552  lincreslvec3  46553  isldepslvec2  46556  zlmodzxzldeplem3  46573  1arympt1  46714  ackendofnn0  46760  aacllem  47238