Theorem ffvelcdm 7033

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ran crn 5632   Fn wfn 6493  ⟶wf 6494  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506

This theorem is referenced by:  ffvelcdmi  7035  ffvelcdmda  7036  dffo3  7054  dffo3f  7058  foco2  7061  ffnfv  7071  ffvresb  7078  fcompt  7086  fsn2  7089  fvconst  7117  fprb  7149  f1cofveqaeq  7212  fcofo  7243  cocan1  7246  fvf1pr  7262  isocnv  7285  isocnv3  7287  isores2  7288  isopolem  7300  isosolem  7302  fovcdm  7537  off  7649  fnwelem  8081  soseq  8109  smofvon2  8296  smocdmdom  8308  omsmolem  8593  omsmo  8594  fsetfcdm  8807  mapfvd  8827  mapsncnv  8841  2dom  8977  xpdom2  9010  domunsncan  9015  xpmapenlem  9082  fiint  9237  infdifsn  9578  cantnflem1  9610  wemapwe  9618  cnfcom3lem  9624  updjudhf  9855  fseqenlem1  9946  finacn  9972  ackbij1lem12  10152  cofsmo  10191  cfsmolem  10192  cfcoflem  10194  coftr  10195  isf32lem6  10280  isf32lem7  10281  isf34lem7  10301  isf34lem6  10302  acncc  10362  axdc2lem  10370  axdc3lem2  10373  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  ttukeylem6  10436  alephreg  10505  pwcfsdom  10506  canthp1lem2  10576  canthp1  10577  pwfseqlem1  10581  pwfseqlem4a  10584  gruf  10734  fsequb2  13938  axdc4uzlem  13945  seqf1o  14005  hashf1lem1  14417  wwlktovf  14918  shftf  15041  limsupgre  15443  rlimuni  15512  lo1resb  15526  o1resb  15528  o1of2  15575  o1rlimmul  15581  isercolllem1  15627  isercolllem2  15628  isercolllem3  15629  isercoll  15630  climsup  15632  iseralt  15647  sumeq2ii  15655  summolem2a  15677  isumcl  15723  isumshft  15804  climcndslem2  15815  climcnds  15816  mertenslem2  15850  prodeq2ii  15876  prodmolem2a  15899  iprodcl  15966  rpnnen2lem10  16190  ruclem8  16204  ruclem12  16208  3dvds  16300  smueqlem  16459  nn0seqcvgd  16539  algrf  16542  eucalg  16556  phimullem  16749  pcmpt  16863  pcprod  16866  vdwlem11  16962  vdwnnlem3  16968  ramlb  16990  0ram  16991  ramcl  17000  prmgaplem8  17029  imasaddfnlem  17492  imasaddflem  17494  chnpof1  18596  mgmhmpropd  18666  mhmpropd  18760  smndex1gid  18872  smndex1gidOLD  18873  ghmsub  19199  cntzmhm  19316  f1omvdconj  19421  pj1ghm  19678  gsumzaddlem  19896  gsumzadd  19897  gsummptnn0fzfv  19962  dprdfadd  19997  subgdmdprd  20011  gsumdixp  20298  lspcl  20971  znunit  21543  frlmsslsp  21776  frlmup2  21779  lindfmm  21807  islindf4  21818  psrbaglesupp  21902  psrbaglefi  21906  resspsrmul  21954  evlslem4  22054  evlslem3  22058  fvcoe1  22171  psropprmul  22201  00ply1bas  22203  subrgvr1cl  22227  coe1mul2lem1  22232  coe1tmmul  22242  ply1coe  22263  evl1val  22294  evl1sca  22299  pf1const  22311  1mavmul  22513  mavmulass  22514  marepvcl  22534  1marepvmarrepid  22540  cramerimplem1  22648  pmatcollpw3fi1lem1  22751  pmatcollpw3fi1lem2  22752  cpmadugsumlemF  22841  cpmadugsumfi  22842  cayleyhamilton1  22857  hauscmplem  23371  ptbasid  23540  ptpjcn  23576  upxp  23588  uptx  23590  txcmplem2  23607  xkopt  23620  txhmeo  23768  alexsubALTlem3  24014  nrginvrcn  24657  nmoi  24693  nmoleub  24696  cncfmet  24876  cnheibor  24922  evth  24926  pcopt  24989  pcopt2  24990  pcorevlem  24993  pi1xfrf  25020  pi1xfr  25022  pi1xfrcnvlem  25023  iscauf  25247  iscmet3lem1  25258  iscmet3lem2  25259  iscmet3  25260  causs  25265  bcthlem5  25295  bcth3  25298  ovolfcl  25433  ovolfioo  25434  ovolficc  25435  ovolficcss  25436  ovolfsval  25437  ovolmge0  25444  ovollb2lem  25455  ovolunlem1a  25463  ovoliunlem1  25469  ovoliunlem2  25470  ovoliun  25472  ovolicc1  25483  ovolicc2lem3  25486  ovolicc2lem4  25487  ovolicc2lem5  25488  voliunlem1  25517  volsup  25523  ioombl1lem2  25526  ovolfs2  25538  uniioovol  25546  uniiccvol  25547  uniioombllem3a  25551  uniioombllem3  25552  uniioombllem4  25553  uniioombllem5  25554  uniioombllem6  25555  dyadmbl  25567  volcn  25573  ismbf  25595  mbfadd  25628  mbfsub  25629  mbflimsup  25633  0plef  25639  itg1climres  25681  mbfi1fseqlem1  25682  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1fseqlem5  25686  mbfmul  25693  xrge0f  25698  itg2ge0  25702  itg2seq  25709  itg2uba  25710  itg2lea  25711  itg2eqa  25712  itg2splitlem  25715  itg2split  25716  itg2i1fseqle  25721  itg2i1fseq  25722  itg2i1fseq2  25723  itg2addlem  25725  bddmulibl  25806  ellimc3  25846  dvaddbr  25905  dvcobr  25913  dvcj  25917  dvfre  25918  dvcnvlem  25943  dvlip  25960  dvlipcn  25961  c1lip1  25964  tdeglem4  26025  tdeglem2  26026  coe1mul3  26064  ply1rem  26131  fta1g  26135  ig1pdvds  26145  plyf  26163  plyeq0lem  26175  plypf1  26177  plyaddlem  26180  plymullem  26181  plyco  26206  dgreq  26209  0dgrb  26211  coefv0  26213  coeaddlem  26214  coemullem  26215  coemulc  26220  plycn  26226  dgrcolem2  26239  plycjlem  26241  plycj  26242  plycjOLD  26244  plyrecj  26246  plyreres  26249  dvply1  26250  vieta1lem2  26277  vieta1  26278  elqaalem2  26286  aareccl  26292  aalioulem1  26298  ulmcaulem  26359  ulmcau  26360  ulmcn  26364  mtest  26369  psergf  26377  dvradcnv  26386  psercn2  26388  pserdvlem2  26393  pserdv2  26395  abelthlem6  26401  abelthlem8  26404  abelthlem9  26405  logtayl  26624  amgm  26954  ftalem1  27036  ftalem2  27037  ftalem3  27038  ftalem4  27039  ftalem5  27040  basellem2  27045  muinv  27156  dchrmulcl  27212  dchrinvcl  27216  dchrfi  27218  dchrghm  27219  dchrsum2  27231  dchrsum  27232  bposlem5  27251  lgscllem  27267  lgsval4a  27282  lgsneg  27284  lgsdir  27295  lgsdilem2  27296  lgsdi  27297  lgsne0  27298  lgseisenlem3  27340  rpvmasumlem  27450  dchrmusum2  27457  dchrvmasumiflem1  27464  dchrisum0ff  27470  dchrisum0flblem1  27471  dchrisum0fno1  27474  rpvmasum2  27475  dchrisum0re  27476  dchrisum0lem2a  27480  upgrreslem  29373  umgrreslem  29374  wlkpvtx  29726  wlkepvtx  29727  usgr2pthlem  29831  frgrncvvdeqlem8  30376  lnoadd  30829  lnosub  30830  nmosetre  30835  nmooge0  30838  nmoub3i  30844  nmounbi  30847  phoeqi  30928  ubthlem1  30941  h2hcau  31050  h2hlm  31051  hoscl  31816  homcl  31817  hodcl  31818  hoaddcl  31829  homulcl  31830  homullid  31871  homco1  31872  homulass  31873  hoadddi  31874  hoadddir  31875  hoeq1  31901  hoeq2  31902  adjsym  31904  nmopsetretALT  31934  nmfnsetre  31948  cnvadj  31963  hhcno  31975  hhcnf  31976  nmopub2tALT  31980  nmopge0  31982  unopf1o  31987  unoplin  31991  counop  31992  nmfnleub2  31997  nmfnge0  31998  hmoplin  32013  eigvalcl  32032  lnop0  32037  hmops  32091  hmopm  32092  nlelchi  32132  leop2  32195  leopadd  32203  leopmuli  32204  leopnmid  32209  hmopidmchi  32222  pjinvari  32262  sticl  32286  fcomptf  32731  rge0scvg  34093  esumcst  34207  esumfzf  34213  esumfsup  34214  esumfsupre  34215  hasheuni  34229  measdivcstALTV  34369  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemb  34512  derangsn  35352  subfacp1lem5  35366  subfacp1lem6  35367  pconnconn  35413  sconnpi1  35421  txsconnlem  35422  cvxsconn  35425  cvmliftphtlem  35499  cvmlift3lem2  35502  cvmlift3lem4  35504  cvmlift3lem6  35506  satfvel  35594  satefvfmla1  35607  elmrsubrn  35702  msubff  35712  msubvrs  35742  mclsssvlem  35744  faclim  35928  curf  37919  uncf  37920  curunc  37923  unccur  37924  matunitlindflem1  37937  matunitlindflem2  37938  ptrecube  37941  heicant  37976  mblfinlem2  37979  itg2addnclem  37992  ftc1anclem1  38014  ftc1anclem2  38015  ftc1anclem4  38017  upixp  38050  fdc  38066  seqpo  38068  incsequz  38069  incsequz2  38070  metf1o  38076  geomcau  38080  sstotbnd2  38095  prdsbnd  38114  ismtyima  38124  ismtyhmeolem  38125  heiborlem3  38134  heiborlem6  38137  heiborlem10  38141  bfplem1  38143  ghomco  38212  sticksstones11  42595  mzpclall  43159  mzprename  43181  rexrabdioph  43222  rmydioph  43442  rmxdioph  43444  expdiophlem2  43450  expdioph  43451  pw2f1ocnv  43465  kelac1  43491  rngunsnply  43597  ofsubid  44751  ofdivrec  44753  ofdivcan4  44754  ofdivdiv2  44755  dvconstbi  44761  refsum2cnlem1  45468  climinf  46036  stoweidlem26  46454  stoweidlem60  46488  stoweid  46491  dmvolsal  46774  caratheodory  46956  elhoi  46970  smfresal  47216  f1oresf1o2  47739  fargshiftf  47900  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  isubgrvtxuhgr  48340  isubgruhgr  48344  isubgr0uhgr  48349  grimuhgr  48363  gricushgr  48393  rmsupp0  48844  domnmsuppn0  48845  gsumlsscl  48856  lincfsuppcl  48889  linccl  48890  lincdifsn  48900  lincsum  48905  lincscm  48906  lincscmcl  48908  lincext1  48930  lindslinindimp2lem1  48934  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  snlindsntor  48947  lincresunitlem2  48952  lincresunit3lem1  48955  lincresunit3lem2  48956  lincresunit3  48957  lincreslvec3  48958  isldepslvec2  48961  zlmodzxzldeplem3  48978  1arympt1  49114  ackendofnn0  49160  xpco2  49332  aacllem  50276