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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5660   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 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  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  7120  fcompt  7128  fsn2  7131  fvconst  7159  fprb  7191  f1cofveqaeq  7255  fcofo  7286  cocan1  7289  fvf1pr  7305  isocnv  7328  isocnv3  7330  isores2  7331  isopolem  7343  isosolem  7345  fovcdm  7582  off  7694  fnwelem  8135  soseq  8163  smofvon2  8375  smocdmdom  8387  omsmolem  8674  omsmo  8675  fsetfcdm  8879  mapfvd  8898  mapsncnv  8912  2dom  9049  xpdom2  9086  domunsncan  9091  xpmapenlem  9163  fiint  9343  fiintOLD  9344  infdifsn  9676  cantnflem1  9708  wemapwe  9716  cnfcom3lem  9722  updjudhf  9950  fseqenlem1  10043  finacn  10069  ackbij1lem12  10249  cofsmo  10288  cfsmolem  10289  cfcoflem  10291  coftr  10292  isf32lem6  10377  isf32lem7  10378  isf34lem7  10398  isf34lem6  10399  acncc  10459  axdc2lem  10467  axdc3lem2  10470  axdc3lem4  10472  axdc4lem  10474  axcclem  10476  ttukeylem6  10533  alephreg  10601  pwcfsdom  10602  canthp1lem2  10672  canthp1  10673  pwfseqlem1  10677  pwfseqlem4a  10680  gruf  10830  fsequb2  13999  axdc4uzlem  14006  seqf1o  14066  hashf1lem1  14478  wwlktovf  14980  shftf  15103  limsupgre  15502  rlimuni  15571  lo1resb  15585  o1resb  15587  o1of2  15634  o1rlimmul  15640  isercolllem1  15686  isercolllem2  15687  isercolllem3  15688  isercoll  15689  climsup  15691  iseralt  15706  sumeq2ii  15714  summolem2a  15736  isumcl  15782  isumshft  15860  climcndslem2  15871  climcnds  15872  mertenslem2  15906  prodeq2ii  15932  prodmolem2a  15955  iprodcl  16022  rpnnen2lem10  16246  ruclem8  16260  ruclem12  16264  3dvds  16355  smueqlem  16514  nn0seqcvgd  16594  algrf  16597  eucalg  16611  phimullem  16803  pcmpt  16917  pcprod  16920  vdwlem11  17016  vdwnnlem3  17022  ramlb  17044  0ram  17045  ramcl  17054  prmgaplem8  17083  imasaddfnlem  17547  imasaddflem  17549  mgmhmpropd  18681  mhmpropd  18775  smndex1gid  18886  ghmsub  19212  cntzmhm  19329  f1omvdconj  19432  pj1ghm  19689  gsumzaddlem  19907  gsumzadd  19908  gsummptnn0fzfv  19973  dprdfadd  20008  subgdmdprd  20022  gsumdixp  20284  lspcl  20938  znunit  21529  frlmsslsp  21761  frlmup2  21764  lindfmm  21792  islindf4  21803  psrbaglesupp  21887  psrbaglefi  21891  resspsrmul  21941  evlslem4  22039  evlslem3  22043  fvcoe1  22148  psropprmul  22178  00ply1bas  22180  subrgvr1cl  22204  coe1mul2lem1  22209  coe1tmmul  22219  ply1coe  22241  evl1val  22272  evl1sca  22277  pf1const  22289  1mavmul  22491  mavmulass  22492  marepvcl  22512  1marepvmarrepid  22518  cramerimplem1  22626  pmatcollpw3fi1lem1  22729  pmatcollpw3fi1lem2  22730  cpmadugsumlemF  22819  cpmadugsumfi  22820  cayleyhamilton1  22835  hauscmplem  23349  ptbasid  23518  ptpjcn  23554  upxp  23566  uptx  23568  txcmplem2  23585  xkopt  23598  txhmeo  23746  alexsubALTlem3  23992  nrginvrcn  24636  nmoi  24672  nmoleub  24675  cncfmet  24858  cnheibor  24910  evth  24914  pcopt  24978  pcopt2  24979  pcorevlem  24982  pi1xfrf  25009  pi1xfr  25011  pi1xfrcnvlem  25012  iscauf  25237  iscmet3lem1  25248  iscmet3lem2  25249  iscmet3  25250  causs  25255  bcthlem5  25285  bcth3  25288  ovolfcl  25424  ovolfioo  25425  ovolficc  25426  ovolficcss  25427  ovolfsval  25428  ovolmge0  25435  ovollb2lem  25446  ovolunlem1a  25454  ovoliunlem1  25460  ovoliunlem2  25461  ovoliun  25463  ovolicc1  25474  ovolicc2lem3  25477  ovolicc2lem4  25478  ovolicc2lem5  25479  voliunlem1  25508  volsup  25514  ioombl1lem2  25517  ovolfs2  25529  uniioovol  25537  uniiccvol  25538  uniioombllem3a  25542  uniioombllem3  25543  uniioombllem4  25544  uniioombllem5  25545  uniioombllem6  25546  dyadmbl  25558  volcn  25564  ismbf  25586  mbfadd  25619  mbfsub  25620  mbflimsup  25624  0plef  25630  itg1climres  25672  mbfi1fseqlem1  25673  mbfi1fseqlem3  25675  mbfi1fseqlem4  25676  mbfi1fseqlem5  25677  mbfmul  25684  xrge0f  25689  itg2ge0  25693  itg2seq  25700  itg2uba  25701  itg2lea  25702  itg2eqa  25703  itg2splitlem  25706  itg2split  25707  itg2i1fseqle  25712  itg2i1fseq  25713  itg2i1fseq2  25714  itg2addlem  25716  bddmulibl  25797  ellimc3  25837  dvaddbr  25897  dvcobr  25906  dvcobrOLD  25907  dvcj  25911  dvfre  25912  dvcnvlem  25937  dvlip  25955  dvlipcn  25956  c1lip1  25959  tdeglem4  26022  tdeglem2  26023  coe1mul3  26061  ply1rem  26128  fta1g  26132  ig1pdvds  26142  plyf  26160  plyeq0lem  26172  plypf1  26174  plyaddlem  26177  plymullem  26178  plyco  26203  dgreq  26206  0dgrb  26208  coefv0  26210  coeaddlem  26211  coemullem  26212  coemulc  26217  plycn  26223  plycnOLD  26224  dgrcolem2  26237  plycjlem  26239  plycj  26240  plycjOLD  26242  plyrecj  26244  plyreres  26247  dvply1  26248  vieta1lem2  26276  vieta1  26277  elqaalem2  26285  aareccl  26291  aalioulem1  26297  ulmcaulem  26360  ulmcau  26361  ulmcn  26365  mtest  26370  psergf  26378  dvradcnv  26387  psercn2  26389  psercn2OLD  26390  pserdvlem2  26395  pserdv2  26397  abelthlem6  26403  abelthlem8  26406  abelthlem9  26407  logtayl  26626  amgm  26958  ftalem1  27040  ftalem2  27041  ftalem3  27042  ftalem4  27043  ftalem5  27044  basellem2  27049  muinv  27160  dchrmulcl  27217  dchrinvcl  27221  dchrfi  27223  dchrghm  27224  dchrsum2  27236  dchrsum  27237  bposlem5  27256  lgscllem  27272  lgsval4a  27287  lgsneg  27289  lgsdir  27300  lgsdilem2  27301  lgsdi  27302  lgsne0  27303  lgseisenlem3  27345  rpvmasumlem  27455  dchrmusum2  27462  dchrvmasumiflem1  27469  dchrisum0ff  27475  dchrisum0flblem1  27476  dchrisum0fno1  27479  rpvmasum2  27480  dchrisum0re  27481  dchrisum0lem2a  27485  upgrreslem  29288  umgrreslem  29289  wlkpvtx  29644  wlkepvtx  29645  usgr2pthlem  29750  frgrncvvdeqlem8  30292  lnoadd  30744  lnosub  30745  nmosetre  30750  nmooge0  30753  nmoub3i  30759  nmounbi  30762  phoeqi  30843  ubthlem1  30856  h2hcau  30965  h2hlm  30966  hoscl  31731  homcl  31732  hodcl  31733  hoaddcl  31744  homulcl  31745  homullid  31786  homco1  31787  homulass  31788  hoadddi  31789  hoadddir  31790  hoeq1  31816  hoeq2  31817  adjsym  31819  nmopsetretALT  31849  nmfnsetre  31863  cnvadj  31878  hhcno  31890  hhcnf  31891  nmopub2tALT  31895  nmopge0  31897  unopf1o  31902  unoplin  31906  counop  31907  nmfnleub2  31912  nmfnge0  31913  hmoplin  31928  eigvalcl  31947  lnop0  31952  hmops  32006  hmopm  32007  nlelchi  32047  leop2  32110  leopadd  32118  leopmuli  32119  leopnmid  32124  hmopidmchi  32137  pjinvari  32177  sticl  32201  fcomptf  32641  rge0scvg  33985  esumcst  34099  esumfzf  34105  esumfsup  34106  esumfsupre  34107  hasheuni  34121  measdivcstALTV  34261  eulerpartlems  34397  eulerpartlemgc  34399  eulerpartlemb  34405  derangsn  35197  subfacp1lem5  35211  subfacp1lem6  35212  pconnconn  35258  sconnpi1  35266  txsconnlem  35267  cvxsconn  35270  cvmliftphtlem  35344  cvmlift3lem2  35347  cvmlift3lem4  35349  cvmlift3lem6  35351  satfvel  35439  satefvfmla1  35452  elmrsubrn  35547  msubff  35557  msubvrs  35587  mclsssvlem  35589  faclim  35768  curf  37627  uncf  37628  curunc  37631  unccur  37632  matunitlindflem1  37645  matunitlindflem2  37646  ptrecube  37649  heicant  37684  mblfinlem2  37687  itg2addnclem  37700  ftc1anclem1  37722  ftc1anclem2  37723  ftc1anclem4  37725  upixp  37758  fdc  37774  seqpo  37776  incsequz  37777  incsequz2  37778  metf1o  37784  geomcau  37788  sstotbnd2  37803  prdsbnd  37822  ismtyima  37832  ismtyhmeolem  37833  heiborlem3  37842  heiborlem6  37845  heiborlem10  37849  bfplem1  37851  ghomco  37920  sticksstones11  42174  mzpclall  42725  mzprename  42747  rexrabdioph  42792  rmydioph  43013  rmxdioph  43015  expdiophlem2  43021  expdioph  43022  pw2f1ocnv  43036  kelac1  43062  rngunsnply  43168  ofsubid  44323  ofdivrec  44325  ofdivcan4  44326  ofdivdiv2  44327  dvconstbi  44333  refsum2cnlem1  45041  climinf  45615  stoweidlem26  46035  stoweidlem60  46069  stoweid  46072  dmvolsal  46355  caratheodory  46537  elhoi  46551  smfresal  46797  f1oresf1o2  47300  fargshiftf  47434  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  isubgrvtxuhgr  47857  isubgruhgr  47861  isubgr0uhgr  47866  grimuhgr  47880  gricushgr  47910  rmsupp0  48323  domnmsuppn0  48324  gsumlsscl  48335  lincfsuppcl  48369  linccl  48370  lincdifsn  48380  lincsum  48385  lincscm  48386  lincscmcl  48388  lincext1  48410  lindslinindimp2lem1  48414  lindslinindimp2lem4  48417  lindslinindsimp2lem5  48418  snlindsntor  48427  lincresunitlem2  48432  lincresunit3lem1  48435  lincresunit3lem2  48436  lincresunit3  48437  lincreslvec3  48438  isldepslvec2  48441  zlmodzxzldeplem3  48458  1arympt1  48598  ackendofnn0  48644  aacllem  49645