Theorem ffvelcdm 7100

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ran crn 5689   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570

This theorem is referenced by:  ffvelcdmi  7102  ffvelcdmda  7103  dffo3  7121  dffo3f  7125  foco2  7128  ffnfv  7138  ffvresb  7144  fcompt  7152  fsn2  7155  fvconst  7183  fprb  7213  f1cofveqaeq  7277  2f1fvneq  7279  fcofo  7307  cocan1  7310  fvf1pr  7326  isocnv  7349  isocnv3  7351  isores2  7352  isopolem  7364  isosolem  7366  fovcdm  7602  off  7714  fnwelem  8154  soseq  8182  smofvon2  8394  smocdmdom  8406  omsmolem  8693  omsmo  8694  fsetfcdm  8898  mapfvd  8917  mapsncnv  8931  2dom  9068  xpdom2  9105  domunsncan  9110  xpmapenlem  9182  fiint  9363  fiintOLD  9364  infdifsn  9694  cantnflem1  9726  wemapwe  9734  cnfcom3lem  9740  updjudhf  9968  fseqenlem1  10061  finacn  10087  ackbij1lem12  10267  cofsmo  10306  cfsmolem  10307  cfcoflem  10309  coftr  10310  isf32lem6  10395  isf32lem7  10396  isf34lem7  10416  isf34lem6  10417  acncc  10477  axdc2lem  10485  axdc3lem2  10488  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  ttukeylem6  10551  alephreg  10619  pwcfsdom  10620  canthp1lem2  10690  canthp1  10691  pwfseqlem1  10695  pwfseqlem4a  10698  gruf  10848  fsequb2  14013  axdc4uzlem  14020  seqf1o  14080  hashf1lem1  14490  wwlktovf  14991  shftf  15114  limsupgre  15513  rlimuni  15582  lo1resb  15596  o1resb  15598  o1of2  15645  o1rlimmul  15651  isercolllem1  15697  isercolllem2  15698  isercolllem3  15699  isercoll  15700  climsup  15702  iseralt  15717  sumeq2ii  15725  summolem2a  15747  isumcl  15793  isumshft  15871  climcndslem2  15882  climcnds  15883  mertenslem2  15917  prodeq2ii  15943  prodmolem2a  15966  iprodcl  16033  rpnnen2lem10  16255  ruclem8  16269  ruclem12  16273  3dvds  16364  smueqlem  16523  nn0seqcvgd  16603  algrf  16606  eucalg  16620  phimullem  16812  pcmpt  16925  pcprod  16928  vdwlem11  17024  vdwnnlem3  17030  ramlb  17052  0ram  17053  ramcl  17062  prmgaplem8  17091  imasaddfnlem  17574  imasaddflem  17576  mgmhmpropd  18723  mhmpropd  18817  smndex1gid  18928  ghmsub  19254  cntzmhm  19371  f1omvdconj  19478  pj1ghm  19735  gsumzaddlem  19953  gsumzadd  19954  gsummptnn0fzfv  20019  dprdfadd  20054  subgdmdprd  20068  gsumdixp  20332  lspcl  20991  znunit  21599  frlmsslsp  21833  frlmup2  21836  lindfmm  21864  islindf4  21875  psrbaglesupp  21959  psrbaglefi  21963  resspsrmul  22013  evlslem4  22117  evlslem3  22121  fvcoe1  22224  psropprmul  22254  00ply1bas  22256  subrgvr1cl  22280  coe1mul2lem1  22285  coe1tmmul  22295  ply1coe  22317  evl1val  22348  evl1sca  22353  pf1const  22365  1mavmul  22569  mavmulass  22570  marepvcl  22590  1marepvmarrepid  22596  cramerimplem1  22704  pmatcollpw3fi1lem1  22807  pmatcollpw3fi1lem2  22808  cpmadugsumlemF  22897  cpmadugsumfi  22898  cayleyhamilton1  22913  hauscmplem  23429  ptbasid  23598  ptpjcn  23634  upxp  23646  uptx  23648  txcmplem2  23665  xkopt  23678  txhmeo  23826  alexsubALTlem3  24072  nrginvrcn  24728  nmoi  24764  nmoleub  24767  cncfmet  24948  cnheibor  25000  evth  25004  pcopt  25068  pcopt2  25069  pcorevlem  25072  pi1xfrf  25099  pi1xfr  25101  pi1xfrcnvlem  25102  iscauf  25327  iscmet3lem1  25338  iscmet3lem2  25339  iscmet3  25340  causs  25345  bcthlem5  25375  bcth3  25378  ovolfcl  25514  ovolfioo  25515  ovolficc  25516  ovolficcss  25517  ovolfsval  25518  ovolmge0  25525  ovollb2lem  25536  ovolunlem1a  25544  ovoliunlem1  25550  ovoliunlem2  25551  ovoliun  25553  ovolicc1  25564  ovolicc2lem3  25567  ovolicc2lem4  25568  ovolicc2lem5  25569  voliunlem1  25598  volsup  25604  ioombl1lem2  25607  ovolfs2  25619  uniioovol  25627  uniiccvol  25628  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  uniioombllem6  25636  dyadmbl  25648  volcn  25654  ismbf  25676  mbfadd  25709  mbfsub  25710  mbflimsup  25714  0plef  25720  itg1climres  25763  mbfi1fseqlem1  25764  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfmul  25775  xrge0f  25780  itg2ge0  25784  itg2seq  25791  itg2uba  25792  itg2lea  25793  itg2eqa  25794  itg2splitlem  25797  itg2split  25798  itg2i1fseqle  25803  itg2i1fseq  25804  itg2i1fseq2  25805  itg2addlem  25807  bddmulibl  25888  ellimc3  25928  dvaddbr  25988  dvcobr  25997  dvcobrOLD  25998  dvcj  26002  dvfre  26003  dvcnvlem  26028  dvlip  26046  dvlipcn  26047  c1lip1  26050  tdeglem4  26113  tdeglem2  26114  coe1mul3  26152  ply1rem  26219  fta1g  26223  ig1pdvds  26233  plyf  26251  plyeq0lem  26263  plypf1  26265  plyaddlem  26268  plymullem  26269  plyco  26294  dgreq  26297  0dgrb  26299  coefv0  26301  coeaddlem  26302  coemullem  26303  coemulc  26308  plycn  26314  plycnOLD  26315  dgrcolem2  26328  plycjlem  26330  plycj  26331  plycjOLD  26333  plyrecj  26335  plyreres  26338  dvply1  26339  vieta1lem2  26367  vieta1  26368  elqaalem2  26376  aareccl  26382  aalioulem1  26388  ulmcaulem  26451  ulmcau  26452  ulmcn  26456  mtest  26461  psergf  26469  dvradcnv  26478  psercn2  26480  psercn2OLD  26481  pserdvlem2  26486  pserdv2  26488  abelthlem6  26494  abelthlem8  26497  abelthlem9  26498  logtayl  26716  amgm  27048  ftalem1  27130  ftalem2  27131  ftalem3  27132  ftalem4  27133  ftalem5  27134  basellem2  27139  muinv  27250  dchrmulcl  27307  dchrinvcl  27311  dchrfi  27313  dchrghm  27314  dchrsum2  27326  dchrsum  27327  bposlem5  27346  lgscllem  27362  lgsval4a  27377  lgsneg  27379  lgsdir  27390  lgsdilem2  27391  lgsdi  27392  lgsne0  27393  lgseisenlem3  27435  rpvmasumlem  27545  dchrmusum2  27552  dchrvmasumiflem1  27559  dchrisum0ff  27565  dchrisum0flblem1  27566  dchrisum0fno1  27569  rpvmasum2  27570  dchrisum0re  27571  dchrisum0lem2a  27575  upgrreslem  29335  umgrreslem  29336  wlkpvtx  29691  wlkepvtx  29692  usgr2pthlem  29795  frgrncvvdeqlem8  30334  lnoadd  30786  lnosub  30787  nmosetre  30792  nmooge0  30795  nmoub3i  30801  nmounbi  30804  phoeqi  30885  ubthlem1  30898  h2hcau  31007  h2hlm  31008  hoscl  31773  homcl  31774  hodcl  31775  hoaddcl  31786  homulcl  31787  homullid  31828  homco1  31829  homulass  31830  hoadddi  31831  hoadddir  31832  hoeq1  31858  hoeq2  31859  adjsym  31861  nmopsetretALT  31891  nmfnsetre  31905  cnvadj  31920  hhcno  31932  hhcnf  31933  nmopub2tALT  31937  nmopge0  31939  unopf1o  31944  unoplin  31948  counop  31949  nmfnleub2  31954  nmfnge0  31955  hmoplin  31970  eigvalcl  31989  lnop0  31994  hmops  32048  hmopm  32049  nlelchi  32089  leop2  32152  leopadd  32160  leopmuli  32161  leopnmid  32166  hmopidmchi  32179  pjinvari  32219  sticl  32243  fcomptf  32674  rge0scvg  33909  esumcst  34043  esumfzf  34049  esumfsup  34050  esumfsupre  34051  hasheuni  34065  measdivcstALTV  34205  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemb  34349  derangsn  35154  subfacp1lem5  35168  subfacp1lem6  35169  pconnconn  35215  sconnpi1  35223  txsconnlem  35224  cvxsconn  35227  cvmliftphtlem  35301  cvmlift3lem2  35304  cvmlift3lem4  35306  cvmlift3lem6  35308  satfvel  35396  satefvfmla1  35409  elmrsubrn  35504  msubff  35514  msubvrs  35544  mclsssvlem  35546  faclim  35725  curf  37584  uncf  37585  curunc  37588  unccur  37589  matunitlindflem1  37602  matunitlindflem2  37603  ptrecube  37606  heicant  37641  mblfinlem2  37644  itg2addnclem  37657  ftc1anclem1  37679  ftc1anclem2  37680  ftc1anclem4  37682  upixp  37715  fdc  37731  seqpo  37733  incsequz  37734  incsequz2  37735  metf1o  37741  geomcau  37745  sstotbnd2  37760  prdsbnd  37779  ismtyima  37789  ismtyhmeolem  37790  heiborlem3  37799  heiborlem6  37802  heiborlem10  37806  bfplem1  37808  ghomco  37877  sticksstones11  42137  mzpclall  42714  mzprename  42736  rexrabdioph  42781  rmydioph  43002  rmxdioph  43004  expdiophlem2  43010  expdioph  43011  pw2f1ocnv  43025  kelac1  43051  rngunsnply  43157  ofsubid  44319  ofdivrec  44321  ofdivcan4  44322  ofdivdiv2  44323  dvconstbi  44329  refsum2cnlem1  44974  climinf  45561  stoweidlem26  45981  stoweidlem60  46015  stoweid  46018  dmvolsal  46301  caratheodory  46483  elhoi  46497  smfresal  46743  f1oresf1o2  47240  fargshiftf  47364  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  isubgrvtxuhgr  47787  isubgruhgr  47791  isubgr0uhgr  47796  grimuhgr  47815  gricushgr  47823  rmsupp0  48212  domnmsuppn0  48213  gsumlsscl  48224  lincfsuppcl  48258  linccl  48259  lincdifsn  48269  lincsum  48274  lincscm  48275  lincscmcl  48277  lincext1  48299  lindslinindimp2lem1  48303  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  snlindsntor  48316  lincresunitlem2  48321  lincresunit3lem1  48324  lincresunit3lem2  48325  lincresunit3  48326  lincreslvec3  48327  isldepslvec2  48330  zlmodzxzldeplem3  48347  1arympt1  48487  ackendofnn0  48533  aacllem  49031