Theorem ffvelcdm 7115

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ran crn 5701   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581

This theorem is referenced by:  ffvelcdmi  7117  ffvelcdmda  7118  dffo3  7136  dffo3f  7140  foco2  7143  ffnfv  7153  ffvresb  7159  fcompt  7167  fsn2  7170  fvconst  7198  fprb  7231  f1cofveqaeq  7295  2f1fvneq  7297  fcofo  7324  cocan1  7327  fvf1pr  7343  isocnv  7366  isocnv3  7368  isores2  7369  isopolem  7381  isosolem  7383  fovcdm  7620  off  7732  fnwelem  8172  soseq  8200  smofvon2  8412  smocdmdom  8424  omsmolem  8713  omsmo  8714  fsetfcdm  8918  mapfvd  8937  mapsncnv  8951  2dom  9095  xpdom2  9133  domunsncan  9138  xpmapenlem  9210  fiint  9394  fiintOLD  9395  infdifsn  9726  cantnflem1  9758  wemapwe  9766  cnfcom3lem  9772  updjudhf  10000  fseqenlem1  10093  finacn  10119  ackbij1lem12  10299  cofsmo  10338  cfsmolem  10339  cfcoflem  10341  coftr  10342  isf32lem6  10427  isf32lem7  10428  isf34lem7  10448  isf34lem6  10449  acncc  10509  axdc2lem  10517  axdc3lem2  10520  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  ttukeylem6  10583  alephreg  10651  pwcfsdom  10652  canthp1lem2  10722  canthp1  10723  pwfseqlem1  10727  pwfseqlem4a  10730  gruf  10880  fsequb2  14027  axdc4uzlem  14034  seqf1o  14094  hashf1lem1  14504  wwlktovf  15005  shftf  15128  limsupgre  15527  rlimuni  15596  lo1resb  15610  o1resb  15612  o1of2  15659  o1rlimmul  15665  isercolllem1  15713  isercolllem2  15714  isercolllem3  15715  isercoll  15716  climsup  15718  iseralt  15733  sumeq2ii  15741  summolem2a  15763  isumcl  15809  isumshft  15887  climcndslem2  15898  climcnds  15899  mertenslem2  15933  prodeq2ii  15959  prodmolem2a  15982  iprodcl  16049  rpnnen2lem10  16271  ruclem8  16285  ruclem12  16289  3dvds  16379  smueqlem  16536  nn0seqcvgd  16617  algrf  16620  eucalg  16634  phimullem  16826  pcmpt  16939  pcprod  16942  vdwlem11  17038  vdwnnlem3  17044  ramlb  17066  0ram  17067  ramcl  17076  prmgaplem8  17105  imasaddfnlem  17588  imasaddflem  17590  mgmhmpropd  18736  mhmpropd  18827  smndex1gid  18938  ghmsub  19264  cntzmhm  19381  f1omvdconj  19488  pj1ghm  19745  gsumzaddlem  19963  gsumzadd  19964  gsummptnn0fzfv  20029  dprdfadd  20064  subgdmdprd  20078  gsumdixp  20342  lspcl  20997  znunit  21605  frlmsslsp  21839  frlmup2  21842  lindfmm  21870  islindf4  21881  psrbaglesupp  21965  psrbaglefi  21969  resspsrmul  22019  evlslem4  22123  evlslem3  22127  fvcoe1  22230  psropprmul  22260  00ply1bas  22262  subrgvr1cl  22286  coe1mul2lem1  22291  coe1tmmul  22301  ply1coe  22323  evl1val  22354  evl1sca  22359  pf1const  22371  1mavmul  22575  mavmulass  22576  marepvcl  22596  1marepvmarrepid  22602  cramerimplem1  22710  pmatcollpw3fi1lem1  22813  pmatcollpw3fi1lem2  22814  cpmadugsumlemF  22903  cpmadugsumfi  22904  cayleyhamilton1  22919  hauscmplem  23435  ptbasid  23604  ptpjcn  23640  upxp  23652  uptx  23654  txcmplem2  23671  xkopt  23684  txhmeo  23832  alexsubALTlem3  24078  nrginvrcn  24734  nmoi  24770  nmoleub  24773  cncfmet  24954  cnheibor  25006  evth  25010  pcopt  25074  pcopt2  25075  pcorevlem  25078  pi1xfrf  25105  pi1xfr  25107  pi1xfrcnvlem  25108  iscauf  25333  iscmet3lem1  25344  iscmet3lem2  25345  iscmet3  25346  causs  25351  bcthlem5  25381  bcth3  25384  ovolfcl  25520  ovolfioo  25521  ovolficc  25522  ovolficcss  25523  ovolfsval  25524  ovolmge0  25531  ovollb2lem  25542  ovolunlem1a  25550  ovoliunlem1  25556  ovoliunlem2  25557  ovoliun  25559  ovolicc1  25570  ovolicc2lem3  25573  ovolicc2lem4  25574  ovolicc2lem5  25575  voliunlem1  25604  volsup  25610  ioombl1lem2  25613  ovolfs2  25625  uniioovol  25633  uniiccvol  25634  uniioombllem3a  25638  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  uniioombllem6  25642  dyadmbl  25654  volcn  25660  ismbf  25682  mbfadd  25715  mbfsub  25716  mbflimsup  25720  0plef  25726  itg1climres  25769  mbfi1fseqlem1  25770  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1fseqlem5  25774  mbfmul  25781  xrge0f  25786  itg2ge0  25790  itg2seq  25797  itg2uba  25798  itg2lea  25799  itg2eqa  25800  itg2splitlem  25803  itg2split  25804  itg2i1fseqle  25809  itg2i1fseq  25810  itg2i1fseq2  25811  itg2addlem  25813  bddmulibl  25894  ellimc3  25934  dvaddbr  25994  dvcobr  26003  dvcobrOLD  26004  dvcj  26008  dvfre  26009  dvcnvlem  26034  dvlip  26052  dvlipcn  26053  c1lip1  26056  tdeglem4  26119  tdeglem2  26120  coe1mul3  26158  ply1rem  26225  fta1g  26229  ig1pdvds  26239  plyf  26257  plyeq0lem  26269  plypf1  26271  plyaddlem  26274  plymullem  26275  plyco  26300  dgreq  26303  0dgrb  26305  coefv0  26307  coeaddlem  26308  coemullem  26309  coemulc  26314  plycn  26320  plycnOLD  26321  dgrcolem2  26334  plycjlem  26336  plycj  26337  plyrecj  26339  plyreres  26342  dvply1  26343  vieta1lem2  26371  vieta1  26372  elqaalem2  26380  aareccl  26386  aalioulem1  26392  ulmcaulem  26455  ulmcau  26456  ulmcn  26460  mtest  26465  psergf  26473  dvradcnv  26482  psercn2  26484  psercn2OLD  26485  pserdvlem2  26490  pserdv2  26492  abelthlem6  26498  abelthlem8  26501  abelthlem9  26502  logtayl  26720  amgm  27052  ftalem1  27134  ftalem2  27135  ftalem3  27136  ftalem4  27137  ftalem5  27138  basellem2  27143  muinv  27254  dchrmulcl  27311  dchrinvcl  27315  dchrfi  27317  dchrghm  27318  dchrsum2  27330  dchrsum  27331  bposlem5  27350  lgscllem  27366  lgsval4a  27381  lgsneg  27383  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  lgseisenlem3  27439  rpvmasumlem  27549  dchrmusum2  27556  dchrvmasumiflem1  27563  dchrisum0ff  27569  dchrisum0flblem1  27570  dchrisum0fno1  27573  rpvmasum2  27574  dchrisum0re  27575  dchrisum0lem2a  27579  upgrreslem  29339  umgrreslem  29340  wlkpvtx  29695  wlkepvtx  29696  usgr2pthlem  29799  frgrncvvdeqlem8  30338  lnoadd  30790  lnosub  30791  nmosetre  30796  nmooge0  30799  nmoub3i  30805  nmounbi  30808  phoeqi  30889  ubthlem1  30902  h2hcau  31011  h2hlm  31012  hoscl  31777  homcl  31778  hodcl  31779  hoaddcl  31790  homulcl  31791  homullid  31832  homco1  31833  homulass  31834  hoadddi  31835  hoadddir  31836  hoeq1  31862  hoeq2  31863  adjsym  31865  nmopsetretALT  31895  nmfnsetre  31909  cnvadj  31924  hhcno  31936  hhcnf  31937  nmopub2tALT  31941  nmopge0  31943  unopf1o  31948  unoplin  31952  counop  31953  nmfnleub2  31958  nmfnge0  31959  hmoplin  31974  eigvalcl  31993  lnop0  31998  hmops  32052  hmopm  32053  nlelchi  32093  leop2  32156  leopadd  32164  leopmuli  32165  leopnmid  32170  hmopidmchi  32183  pjinvari  32223  sticl  32247  fcomptf  32676  rge0scvg  33895  esumcst  34027  esumfzf  34033  esumfsup  34034  esumfsupre  34035  hasheuni  34049  measdivcstALTV  34189  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemb  34333  derangsn  35138  subfacp1lem5  35152  subfacp1lem6  35153  pconnconn  35199  sconnpi1  35207  txsconnlem  35208  cvxsconn  35211  cvmliftphtlem  35285  cvmlift3lem2  35288  cvmlift3lem4  35290  cvmlift3lem6  35292  satfvel  35380  satefvfmla1  35393  elmrsubrn  35488  msubff  35498  msubvrs  35528  mclsssvlem  35530  faclim  35708  curf  37558  uncf  37559  curunc  37562  unccur  37563  matunitlindflem1  37576  matunitlindflem2  37577  ptrecube  37580  heicant  37615  mblfinlem2  37618  itg2addnclem  37631  ftc1anclem1  37653  ftc1anclem2  37654  ftc1anclem4  37656  upixp  37689  fdc  37705  seqpo  37707  incsequz  37708  incsequz2  37709  metf1o  37715  geomcau  37719  sstotbnd2  37734  prdsbnd  37753  ismtyima  37763  ismtyhmeolem  37764  heiborlem3  37773  heiborlem6  37776  heiborlem10  37780  bfplem1  37782  ghomco  37851  sticksstones11  42113  mzpclall  42683  mzprename  42705  rexrabdioph  42750  rmydioph  42971  rmxdioph  42973  expdiophlem2  42979  expdioph  42980  pw2f1ocnv  42994  kelac1  43020  rngunsnply  43130  ofsubid  44293  ofdivrec  44295  ofdivcan4  44296  ofdivdiv2  44297  dvconstbi  44303  refsum2cnlem1  44937  climinf  45527  stoweidlem26  45947  stoweidlem60  45981  stoweid  45984  dmvolsal  46267  caratheodory  46449  elhoi  46463  smfresal  46709  f1oresf1o2  47206  fargshiftf  47314  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  isubgrvtxuhgr  47736  isubgruhgr  47738  isubgr0uhgr  47743  grimuhgr  47762  gricushgr  47770  rmsupp0  48093  domnmsuppn0  48094  gsumlsscl  48108  lincfsuppcl  48142  linccl  48143  lincdifsn  48153  lincsum  48158  lincscm  48159  lincscmcl  48161  lincext1  48183  lindslinindimp2lem1  48187  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  snlindsntor  48200  lincresunitlem2  48205  lincresunit3lem1  48208  lincresunit3lem2  48209  lincresunit3  48210  lincreslvec3  48211  isldepslvec2  48214  zlmodzxzldeplem3  48231  1arympt1  48372  ackendofnn0  48418  aacllem  48895