Theorem ffvelcdm 7077

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 6706	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7076	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6714	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3933	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 16	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ran crn 5660   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  ffvelcdmi  7079  ffvelcdmda  7080  dffo3  7098  dffo3f  7102  foco2  7105  ffnfv  7115  ffvresb  7122  fcompt  7130  fsn2  7133  fvconst  7163  fprb  7195  f1cofveqaeq  7257  fcofo  7292  cocan1  7295  fvf1pr  7311  isocnv  7334  isocnv3  7336  isores2  7337  isopolem  7349  isosolem  7351  fovcdm  7587  off  7699  fnwelem  8132  soseq  8160  smofvon2  8348  smocdmdom  8360  omsmolem  8648  omsmo  8649  fsetfcdm  8864  curf  8872  uncf  8873  mapfvd  8889  mapsncnv  8903  2dom  9040  xpdom2  9073  domunsncan  9078  xpmapenlem  9145  fiint  9299  infdifsn  9639  cantnflem1  9671  wemapwe  9679  cnfcom3lem  9685  updjudhf  9939  fseqenlem1  10030  finacn  10056  ackbij1lem12  10235  cofsmo  10274  cfsmolem  10275  cfcoflem  10277  coftr  10278  isf32lem6  10363  isf32lem7  10364  isf34lem7  10384  isf34lem6  10385  acncc  10445  axdc2lem  10453  axdc3lem2  10456  axdc3lem4  10458  axdc4lem  10460  axcclem  10462  ttukeylem6  10519  alephreg  10594  pwcfsdom  10595  canthp1lem2  10665  canthp1  10666  pwfseqlem1  10670  pwfseqlem4a  10673  gruf  10823  fsequb2  14042  axdc4uzlem  14049  seqf1o  14109  hashf1lem1  14522  wwlktovf  15031  shftf  15154  limsupgre  15570  rlimuni  15639  lo1resb  15653  o1resb  15655  o1of2  15702  o1rlimmul  15708  isercolllem1  15754  isercolllem2  15755  isercolllem3  15756  isercoll  15757  climsup  15759  iseralt  15774  sumeq2ii  15782  summolem2a  15803  isumcl  15849  isumshft  15930  climcndslem2  15941  climcnds  15942  mertenslem2  15976  prodeq2ii  16002  prodmolem2a  16025  iprodcl  16092  rpnnen2lem10  16315  ruclem8  16329  ruclem12  16333  3dvds  16425  smueqlem  16584  nn0seqcvgd  16664  algrf  16667  eucalg  16681  phimullem  16874  pcmpt  16988  pcprod  16991  vdwlem11  17087  vdwnnlem3  17093  ramlb  17115  0ram  17116  ramcl  17125  prmgaplem8  17154  imasaddfnlem  17618  imasaddflem  17620  chnpof1  18722  mgmhmpropd  18802  mhmpropd  18901  smndex1gid  19014  smndex1gidOLD  19015  ghmsub  19352  cntzmhm  19469  f1omvdconj  19574  pj1ghm  19831  gsumzaddlem  20049  gsumzadd  20050  gsummptnn0fzfv  20115  dprdfadd  20150  subgdmdprd  20164  gsumdixp  20460  lspcl  21161  znunit  21777  frlmsslsp  22010  frlmup2  22013  lindfmm  22041  islindf4  22052  psrbaglesupp  22138  psrbaglefi  22142  resspsrmul  22191  evlslem4  22293  evlslem3  22297  fvcoe1  22433  psropprmul  22463  00ply1bas  22465  subrgvr1cl  22489  coe1mul2lem1  22494  coe1tmmul  22504  ply1coe  22524  evl1val  22555  evl1sca  22560  pf1const  22572  1mavmul  22771  mavmulass  22772  marepvcl  22792  1marepvmarrepid  22798  matunitlindflem1  22902  matunitlindflem2  22903  cramerimplem1  22909  pmatcollpw3fi1lem1  23012  pmatcollpw3fi1lem2  23013  cpmadugsumlemF  23102  cpmadugsumfi  23103  cayleyhamilton1  23118  hauscmplem  23632  ptbasid  23802  ptpjcn  23838  upxp  23850  uptx  23852  txcmplem2  23869  xkopt  23882  txhmeo  24030  alexsubALTlem3  24276  nrginvrcn  24919  nmoi  24955  nmoleub  24958  cncfmet  25138  cnheibor  25184  evth  25188  pcopt  25251  pcopt2  25252  pcorevlem  25255  pi1xfrf  25282  pi1xfr  25284  pi1xfrcnvlem  25285  iscauf  25509  iscmet3lem1  25520  iscmet3lem2  25521  iscmet3  25522  causs  25527  bcthlem5  25557  bcth3  25560  ovolfcl  25695  ovolfioo  25696  ovolficc  25697  ovolficcss  25698  ovolfsval  25699  ovolmge0  25706  ovollb2lem  25717  ovolunlem1a  25725  ovoliunlem1  25731  ovoliunlem2  25732  ovoliun  25734  ovolicc1  25745  ovolicc2lem3  25748  ovolicc2lem4  25749  ovolicc2lem5  25750  voliunlem1  25779  volsup  25785  ioombl1lem2  25788  ovolfs2  25800  uniioovol  25808  uniiccvol  25809  uniioombllem3a  25813  uniioombllem3  25814  uniioombllem4  25815  uniioombllem5  25816  uniioombllem6  25817  dyadmbl  25829  volcn  25835  ismbf  25857  mbfadd  25890  mbfsub  25891  mbflimsup  25895  0plef  25901  itg1climres  25943  mbfi1fseqlem1  25944  mbfi1fseqlem3  25946  mbfi1fseqlem4  25947  mbfi1fseqlem5  25948  mbfmul  25955  xrge0f  25960  itg2ge0  25964  itg2seq  25971  itg2uba  25972  itg2lea  25973  itg2eqa  25974  itg2splitlem  25977  itg2split  25978  itg2i1fseqle  25983  itg2i1fseq  25984  itg2i1fseq2  25985  itg2addlem  25987  bddmulibl  26068  ellimc3  26108  dvaddbr  26167  dvcobr  26175  dvcj  26179  dvfre  26180  dvcnvlem  26205  dvlip  26222  dvlipcn  26223  c1lip1  26226  tdeglem4  26287  tdeglem2  26288  coe1mul3  26326  ply1rem  26393  fta1g  26397  ig1pdvds  26407  plyf  26425  plyeq0lem  26437  plypf1  26439  plyaddlem  26442  plymullem  26443  plyco  26468  dgreq  26471  0dgrb  26473  coefv0  26475  coeaddlem  26476  coemullem  26477  coemulc  26482  plycn  26488  dgrcolem2  26501  plycjlem  26503  plycj  26504  plycjOLD  26506  plyrecj  26508  plyreres  26514  dvply1  26515  vieta1lem2  26542  vieta1  26543  elqaalem2  26551  aareccl  26559  aalioulem1  26565  ulmcaulem  26627  ulmcau  26628  ulmcn  26632  mtest  26637  psergf  26645  dvradcnv  26654  psercn2  26656  pserdvlem2  26661  pserdv2  26663  abelthlem6  26669  abelthlem8  26672  abelthlem9  26673  logtayl  26895  amgm  27225  ftalem1  27307  ftalem2  27308  ftalem3  27309  ftalem4  27310  ftalem5  27311  basellem2  27316  muinv  27427  dchrmulcl  27483  dchrinvcl  27487  dchrfi  27489  dchrghm  27490  dchrsum2  27502  dchrsum  27503  bposlem5  27522  lgscllem  27538  lgsval4a  27553  lgsneg  27555  lgsdir  27566  lgsdilem2  27567  lgsdi  27568  lgsne0  27569  lgseisenlem3  27611  rpvmasumlem  27721  dchrmusum2  27728  dchrvmasumiflem1  27735  dchrisum0ff  27741  dchrisum0flblem1  27742  dchrisum0fno1  27745  rpvmasum2  27746  dchrisum0re  27747  dchrisum0lem2a  27751  upgrreslem  29750  umgrreslem  29751  wlkpvtx  30103  wlkepvtx  30104  usgr2pthlem  30214  frgrncvvdeqlem8  30772  lnoadd  31225  lnosub  31226  nmosetre  31231  nmooge0  31234  nmoub3i  31240  nmounbi  31243  phoeqi  31324  ubthlem1  31337  h2hcau  31446  h2hlm  31447  hoscl  32212  homcl  32213  hodcl  32214  hoaddcl  32225  homulcl  32226  homullid  32267  homco1  32268  homulass  32269  hoadddi  32270  hoadddir  32271  hoeq1  32297  hoeq2  32298  adjsym  32300  nmopsetretALT  32330  nmfnsetre  32344  cnvadj  32359  hhcno  32371  hhcnf  32372  nmopub2tALT  32376  nmopge0  32378  unopf1o  32383  unoplin  32387  counop  32388  nmfnleub2  32393  nmfnge0  32394  hmoplin  32409  eigvalcl  32428  lnop0  32433  hmops  32487  hmopm  32488  nlelchi  32528  leop2  32591  leopadd  32599  leopmuli  32600  leopnmid  32605  hmopidmchi  32618  pjinvari  32658  sticl  32682  fcomptf  33118  rge0scvg  34446  esumcst  34560  esumfzf  34566  esumfsup  34567  esumfsupre  34568  hasheuni  34582  measdivcstALTV  34723  eulerpartlems  34858  eulerpartlemgc  34860  eulerpartlemb  34866  derangsn  35736  subfacp1lem5  35750  subfacp1lem6  35751  pconnconn  35797  sconnpi1  35805  txsconnlem  35806  cvxsconn  35809  cvmliftphtlem  35883  cvmlift3lem2  35886  cvmlift3lem4  35888  cvmlift3lem6  35890  satfvel  35978  satefvfmla1  35991  elmrsubrn  36086  msubff  36096  msubvrs  36126  mclsssvlem  36128  faclim  36312  curunc  38343  unccur  38344  ptrecube  38356  heicant  38391  mblfinlem2  38394  itg2addnclem  38407  ftc1anclem1  38429  ftc1anclem2  38430  ftc1anclem4  38432  upixp  38466  fdc  38482  seqpo  38484  incsequz  38485  incsequz2  38486  metf1o  38492  geomcau  38496  sstotbnd2  38511  prdsbnd  38530  ismtyima  38540  ismtyhmeolem  38541  heiborlem3  38550  heiborlem6  38553  heiborlem10  38557  bfplem1  38559  ghomco  38628  sticksstones11  43009  mzpclall  43559  mzprename  43581  rexrabdioph  43622  rmydioph  43842  rmxdioph  43844  expdiophlem2  43850  expdioph  43851  pw2f1ocnv  43865  kelac1  43891  rngunsnply  43997  ofsubid  45135  ofdivrec  45137  ofdivcan4  45138  ofdivdiv2  45139  dvconstbi  45145  refsum2cnlem1  45858  climinf  46423  stoweidlem26  46841  stoweidlem60  46875  stoweid  46878  dmvolsal  47161  caratheodory  47343  elhoi  47357  smfresal  47603  sqrtrrnpoly  47747  f1oresf1o2  48166  fargshiftf  48327  nnsum4primeseven  48703  nnsum4primesevenALTV  48704  isubgrvtxuhgr  48767  isubgruhgr  48771  isubgr0uhgr  48776  grimuhgr  48790  gricushgr  48820  rmsupp0  49285  domnmsuppn0  49286  gsumlsscl  49297  lincfsuppcl  49330  linccl  49331  lincdifsn  49341  lincsum  49346  lincscm  49347  lincscmcl  49349  lincext1  49371  lindslinindimp2lem1  49375  lindslinindimp2lem4  49378  lindslinindsimp2lem5  49379  snlindsntor  49388  lincresunitlem2  49393  lincresunit3lem1  49396  lincresunit3lem2  49397  lincresunit3  49398  lincreslvec3  49399  isldepslvec2  49402  zlmodzxzldeplem3  49419  1arympt1  49555  ackendofnn0  49601  xpco2  49772  aacllem  50759