Theorem ffvelcdm 7076

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 6705	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7075	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 591	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6713	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3935	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 485	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 16	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2141  ran crn 5662   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5256  ax-nul 5268  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2095  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3415  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  ffvelcdmi  7078  ffvelcdmda  7079  dffo3  7097  dffo3f  7101  foco2  7104  ffnfv  7114  ffvresb  7121  fcompt  7129  fsn2  7132  fvconst  7160  fprb  7192  f1cofveqaeq  7255  fcofo  7286  cocan1  7289  fvf1pr  7305  isocnv  7328  isocnv3  7330  isores2  7331  isopolem  7343  isosolem  7345  fovcdm  7580  off  7692  fnwelem  8126  soseq  8154  smofvon2  8342  smocdmdom  8354  omsmolem  8642  omsmo  8643  fsetfcdm  8856  mapfvd  8876  mapsncnv  8890  2dom  9026  xpdom2  9059  domunsncan  9064  xpmapenlem  9131  fiint  9285  infdifsn  9625  cantnflem1  9657  wemapwe  9665  cnfcom3lem  9671  updjudhf  9916  fseqenlem1  10007  finacn  10033  ackbij1lem12  10212  cofsmo  10252  cfsmolem  10253  cfcoflem  10255  coftr  10256  isf32lem6  10341  isf32lem7  10342  isf34lem7  10362  isf34lem6  10363  acncc  10423  axdc2lem  10431  axdc3lem2  10434  axdc3lem4  10436  axdc4lem  10438  axcclem  10440  ttukeylem6  10497  alephreg  10566  pwcfsdom  10567  canthp1lem2  10637  canthp1  10638  pwfseqlem1  10642  pwfseqlem4a  10645  gruf  10795  fsequb2  14011  axdc4uzlem  14018  seqf1o  14078  hashf1lem1  14491  wwlktovf  14992  shftf  15115  limsupgre  15531  rlimuni  15600  lo1resb  15614  o1resb  15616  o1of2  15663  o1rlimmul  15669  isercolllem1  15715  isercolllem2  15716  isercolllem3  15717  isercoll  15718  climsup  15720  iseralt  15735  sumeq2ii  15743  summolem2a  15765  isumcl  15811  isumshft  15892  climcndslem2  15903  climcnds  15904  mertenslem2  15938  prodeq2ii  15964  prodmolem2a  15987  iprodcl  16054  rpnnen2lem10  16278  ruclem8  16292  ruclem12  16296  3dvds  16388  smueqlem  16547  nn0seqcvgd  16627  algrf  16630  eucalg  16644  phimullem  16837  pcmpt  16951  pcprod  16954  vdwlem11  17050  vdwnnlem3  17056  ramlb  17078  0ram  17079  ramcl  17088  prmgaplem8  17117  imasaddfnlem  17581  imasaddflem  17583  chnpof1  18685  mgmhmpropd  18755  mhmpropd  18849  smndex1gid  18962  smndex1gidOLD  18963  ghmsub  19293  cntzmhm  19410  f1omvdconj  19515  pj1ghm  19772  gsumzaddlem  19990  gsumzadd  19991  gsummptnn0fzfv  20056  dprdfadd  20091  subgdmdprd  20105  gsumdixp  20399  lspcl  21076  znunit  21692  frlmsslsp  21925  frlmup2  21928  lindfmm  21956  islindf4  21967  psrbaglesupp  22051  psrbaglefi  22055  resspsrmul  22104  evlslem4  22206  evlslem3  22210  fvcoe1  22346  psropprmul  22376  00ply1bas  22378  subrgvr1cl  22402  coe1mul2lem1  22407  coe1tmmul  22417  ply1coe  22437  evl1val  22468  evl1sca  22473  pf1const  22485  1mavmul  22684  mavmulass  22685  marepvcl  22705  1marepvmarrepid  22711  cramerimplem1  22819  pmatcollpw3fi1lem1  22922  pmatcollpw3fi1lem2  22923  cpmadugsumlemF  23012  cpmadugsumfi  23013  cayleyhamilton1  23028  hauscmplem  23542  ptbasid  23711  ptpjcn  23747  upxp  23759  uptx  23761  txcmplem2  23778  xkopt  23791  txhmeo  23939  alexsubALTlem3  24185  nrginvrcn  24828  nmoi  24864  nmoleub  24867  cncfmet  25047  cnheibor  25093  evth  25097  pcopt  25160  pcopt2  25161  pcorevlem  25164  pi1xfrf  25191  pi1xfr  25193  pi1xfrcnvlem  25194  iscauf  25418  iscmet3lem1  25429  iscmet3lem2  25430  iscmet3  25431  causs  25436  bcthlem5  25466  bcth3  25469  ovolfcl  25604  ovolfioo  25605  ovolficc  25606  ovolficcss  25607  ovolfsval  25608  ovolmge0  25615  ovollb2lem  25626  ovolunlem1a  25634  ovoliunlem1  25640  ovoliunlem2  25641  ovoliun  25643  ovolicc1  25654  ovolicc2lem3  25657  ovolicc2lem4  25658  ovolicc2lem5  25659  voliunlem1  25688  volsup  25694  ioombl1lem2  25697  ovolfs2  25709  uniioovol  25717  uniiccvol  25718  uniioombllem3a  25722  uniioombllem3  25723  uniioombllem4  25724  uniioombllem5  25725  uniioombllem6  25726  dyadmbl  25738  volcn  25744  ismbf  25766  mbfadd  25799  mbfsub  25800  mbflimsup  25804  0plef  25810  itg1climres  25852  mbfi1fseqlem1  25853  mbfi1fseqlem3  25855  mbfi1fseqlem4  25856  mbfi1fseqlem5  25857  mbfmul  25864  xrge0f  25869  itg2ge0  25873  itg2seq  25880  itg2uba  25881  itg2lea  25882  itg2eqa  25883  itg2splitlem  25886  itg2split  25887  itg2i1fseqle  25892  itg2i1fseq  25893  itg2i1fseq2  25894  itg2addlem  25896  bddmulibl  25977  ellimc3  26017  dvaddbr  26076  dvcobr  26084  dvcj  26088  dvfre  26089  dvcnvlem  26114  dvlip  26131  dvlipcn  26132  c1lip1  26135  tdeglem4  26196  tdeglem2  26197  coe1mul3  26235  ply1rem  26302  fta1g  26306  ig1pdvds  26316  plyf  26334  plyeq0lem  26346  plypf1  26348  plyaddlem  26351  plymullem  26352  plyco  26377  dgreq  26380  0dgrb  26382  coefv0  26384  coeaddlem  26385  coemullem  26386  coemulc  26391  plycn  26397  dgrcolem2  26410  plycjlem  26412  plycj  26413  plycjOLD  26415  plyrecj  26417  plyreres  26423  dvply1  26424  vieta1lem2  26451  vieta1  26452  elqaalem2  26460  aareccl  26466  aalioulem1  26472  ulmcaulem  26533  ulmcau  26534  ulmcn  26538  mtest  26543  psergf  26551  dvradcnv  26560  psercn2  26562  pserdvlem2  26567  pserdv2  26569  abelthlem6  26575  abelthlem8  26578  abelthlem9  26579  logtayl  26801  amgm  27131  ftalem1  27213  ftalem2  27214  ftalem3  27215  ftalem4  27216  ftalem5  27217  basellem2  27222  muinv  27333  dchrmulcl  27389  dchrinvcl  27393  dchrfi  27395  dchrghm  27396  dchrsum2  27408  dchrsum  27409  bposlem5  27428  lgscllem  27444  lgsval4a  27459  lgsneg  27461  lgsdir  27472  lgsdilem2  27473  lgsdi  27474  lgsne0  27475  lgseisenlem3  27517  rpvmasumlem  27627  dchrmusum2  27634  dchrvmasumiflem1  27641  dchrisum0ff  27647  dchrisum0flblem1  27648  dchrisum0fno1  27651  rpvmasum2  27652  dchrisum0re  27653  dchrisum0lem2a  27657  upgrreslem  29620  umgrreslem  29621  wlkpvtx  29973  wlkepvtx  29974  usgr2pthlem  30078  frgrncvvdeqlem8  30623  lnoadd  31076  lnosub  31077  nmosetre  31082  nmooge0  31085  nmoub3i  31091  nmounbi  31094  phoeqi  31175  ubthlem1  31188  h2hcau  31297  h2hlm  31298  hoscl  32063  homcl  32064  hodcl  32065  hoaddcl  32076  homulcl  32077  homullid  32118  homco1  32119  homulass  32120  hoadddi  32121  hoadddir  32122  hoeq1  32148  hoeq2  32149  adjsym  32151  nmopsetretALT  32181  nmfnsetre  32195  cnvadj  32210  hhcno  32222  hhcnf  32223  nmopub2tALT  32227  nmopge0  32229  unopf1o  32234  unoplin  32238  counop  32239  nmfnleub2  32244  nmfnge0  32245  hmoplin  32260  eigvalcl  32279  lnop0  32284  hmops  32338  hmopm  32339  nlelchi  32379  leop2  32442  leopadd  32450  leopmuli  32451  leopnmid  32456  hmopidmchi  32469  pjinvari  32509  sticl  32533  fcomptf  32969  rge0scvg  34305  esumcst  34419  esumfzf  34425  esumfsup  34426  esumfsupre  34427  hasheuni  34441  measdivcstALTV  34581  eulerpartlems  34716  eulerpartlemgc  34718  eulerpartlemb  34724  derangsn  35616  subfacp1lem5  35630  subfacp1lem6  35631  pconnconn  35677  sconnpi1  35685  txsconnlem  35686  cvxsconn  35689  cvmliftphtlem  35763  cvmlift3lem2  35766  cvmlift3lem4  35768  cvmlift3lem6  35770  satfvel  35858  satefvfmla1  35871  elmrsubrn  35966  msubff  35976  msubvrs  36006  mclsssvlem  36008  faclim  36192  curf  38193  uncf  38194  curunc  38197  unccur  38198  matunitlindflem1  38211  matunitlindflem2  38212  ptrecube  38215  heicant  38250  mblfinlem2  38253  itg2addnclem  38266  ftc1anclem1  38288  ftc1anclem2  38289  ftc1anclem4  38291  upixp  38324  fdc  38340  seqpo  38342  incsequz  38343  incsequz2  38344  metf1o  38350  geomcau  38354  sstotbnd2  38369  prdsbnd  38388  ismtyima  38398  ismtyhmeolem  38399  heiborlem3  38408  heiborlem6  38411  heiborlem10  38415  bfplem1  38417  ghomco  38486  sticksstones11  42869  mzpclall  43406  mzprename  43428  rexrabdioph  43469  rmydioph  43689  rmxdioph  43691  expdiophlem2  43697  expdioph  43698  pw2f1ocnv  43712  kelac1  43738  rngunsnply  43844  ofsubid  44982  ofdivrec  44984  ofdivcan4  44985  ofdivdiv2  44986  dvconstbi  44992  refsum2cnlem1  45705  climinf  46270  stoweidlem26  46688  stoweidlem60  46722  stoweid  46725  dmvolsal  47008  caratheodory  47190  elhoi  47204  smfresal  47450  f1oresf1o2  47973  fargshiftf  48134  nnsum4primeseven  48510  nnsum4primesevenALTV  48511  isubgrvtxuhgr  48574  isubgruhgr  48578  isubgr0uhgr  48583  grimuhgr  48597  gricushgr  48627  rmsupp0  49093  domnmsuppn0  49094  gsumlsscl  49105  lincfsuppcl  49138  linccl  49139  lincdifsn  49149  lincsum  49154  lincscm  49155  lincscmcl  49157  lincext1  49179  lindslinindimp2lem1  49183  lindslinindimp2lem4  49186  lindslinindsimp2lem5  49187  snlindsntor  49196  lincresunitlem2  49201  lincresunit3lem1  49204  lincresunit3lem2  49205  lincresunit3  49206  lincreslvec3  49207  isldepslvec2  49210  zlmodzxzldeplem3  49227  1arympt1  49363  ackendofnn0  49409  xpco2  49580  aacllem  50546