Theorem ffvelcdm 7064

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 6693	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7063	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 589	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6701	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3937	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 484	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 15	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2144  ran crn 5650   Fn wfn 6518  ⟶wf 6519  ‘cfv 6523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pr 5392

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-fv 6531

This theorem is referenced by:  ffvelcdmi  7066  ffvelcdmda  7067  dffo3  7085  dffo3f  7089  foco2  7092  ffnfv  7102  ffvresb  7109  fcompt  7117  fsn2  7120  fvconst  7148  fprb  7180  f1cofveqaeq  7243  fcofo  7274  cocan1  7277  fvf1pr  7293  isocnv  7316  isocnv3  7318  isores2  7319  isopolem  7331  isosolem  7333  fovcdm  7568  off  7680  fnwelem  8113  soseq  8141  smofvon2  8329  smocdmdom  8341  omsmolem  8629  omsmo  8630  fsetfcdm  8843  mapfvd  8863  mapsncnv  8877  2dom  9013  xpdom2  9046  domunsncan  9051  xpmapenlem  9118  fiint  9273  infdifsn  9614  cantnflem1  9646  wemapwe  9654  cnfcom3lem  9660  updjudhf  9891  fseqenlem1  9982  finacn  10008  ackbij1lem12  10188  cofsmo  10228  cfsmolem  10229  cfcoflem  10231  coftr  10232  isf32lem6  10317  isf32lem7  10318  isf34lem7  10338  isf34lem6  10339  acncc  10399  axdc2lem  10407  axdc3lem2  10410  axdc3lem4  10412  axdc4lem  10414  axcclem  10416  ttukeylem6  10473  alephreg  10542  pwcfsdom  10543  canthp1lem2  10613  canthp1  10614  pwfseqlem1  10618  pwfseqlem4a  10621  gruf  10771  fsequb2  13991  axdc4uzlem  13998  seqf1o  14058  hashf1lem1  14470  wwlktovf  14971  shftf  15094  limsupgre  15510  rlimuni  15579  lo1resb  15593  o1resb  15595  o1of2  15642  o1rlimmul  15648  isercolllem1  15694  isercolllem2  15695  isercolllem3  15696  isercoll  15697  climsup  15699  iseralt  15714  sumeq2ii  15722  summolem2a  15744  isumcl  15790  isumshft  15871  climcndslem2  15882  climcnds  15883  mertenslem2  15917  prodeq2ii  15943  prodmolem2a  15966  iprodcl  16033  rpnnen2lem10  16257  ruclem8  16271  ruclem12  16275  3dvds  16367  smueqlem  16526  nn0seqcvgd  16606  algrf  16609  eucalg  16623  phimullem  16816  pcmpt  16930  pcprod  16933  vdwlem11  17029  vdwnnlem3  17035  ramlb  17057  0ram  17058  ramcl  17067  prmgaplem8  17096  imasaddfnlem  17560  imasaddflem  17562  chnpof1  18664  mgmhmpropd  18734  mhmpropd  18828  smndex1gid  18940  smndex1gidOLD  18941  ghmsub  19266  cntzmhm  19383  f1omvdconj  19488  pj1ghm  19745  gsumzaddlem  19963  gsumzadd  19964  gsummptnn0fzfv  20029  dprdfadd  20064  subgdmdprd  20078  gsumdixp  20369  lspcl  21045  znunit  21617  frlmsslsp  21850  frlmup2  21853  lindfmm  21881  islindf4  21892  psrbaglesupp  21976  psrbaglefi  21980  resspsrmul  22029  evlslem4  22131  evlslem3  22135  fvcoe1  22271  psropprmul  22301  00ply1bas  22303  subrgvr1cl  22327  coe1mul2lem1  22332  coe1tmmul  22342  ply1coe  22363  evl1val  22394  evl1sca  22399  pf1const  22411  1mavmul  22610  mavmulass  22611  marepvcl  22631  1marepvmarrepid  22637  cramerimplem1  22745  pmatcollpw3fi1lem1  22848  pmatcollpw3fi1lem2  22849  cpmadugsumlemF  22938  cpmadugsumfi  22939  cayleyhamilton1  22954  hauscmplem  23468  ptbasid  23637  ptpjcn  23673  upxp  23685  uptx  23687  txcmplem2  23704  xkopt  23717  txhmeo  23865  alexsubALTlem3  24111  nrginvrcn  24754  nmoi  24790  nmoleub  24793  cncfmet  24973  cnheibor  25019  evth  25023  pcopt  25086  pcopt2  25087  pcorevlem  25090  pi1xfrf  25117  pi1xfr  25119  pi1xfrcnvlem  25120  iscauf  25344  iscmet3lem1  25355  iscmet3lem2  25356  iscmet3  25357  causs  25362  bcthlem5  25392  bcth3  25395  ovolfcl  25530  ovolfioo  25531  ovolficc  25532  ovolficcss  25533  ovolfsval  25534  ovolmge0  25541  ovollb2lem  25552  ovolunlem1a  25560  ovoliunlem1  25566  ovoliunlem2  25567  ovoliun  25569  ovolicc1  25580  ovolicc2lem3  25583  ovolicc2lem4  25584  ovolicc2lem5  25585  voliunlem1  25614  volsup  25620  ioombl1lem2  25623  ovolfs2  25635  uniioovol  25643  uniiccvol  25644  uniioombllem3a  25648  uniioombllem3  25649  uniioombllem4  25650  uniioombllem5  25651  uniioombllem6  25652  dyadmbl  25664  volcn  25670  ismbf  25692  mbfadd  25725  mbfsub  25726  mbflimsup  25730  0plef  25736  itg1climres  25778  mbfi1fseqlem1  25779  mbfi1fseqlem3  25781  mbfi1fseqlem4  25782  mbfi1fseqlem5  25783  mbfmul  25790  xrge0f  25795  itg2ge0  25799  itg2seq  25806  itg2uba  25807  itg2lea  25808  itg2eqa  25809  itg2splitlem  25812  itg2split  25813  itg2i1fseqle  25818  itg2i1fseq  25819  itg2i1fseq2  25820  itg2addlem  25822  bddmulibl  25903  ellimc3  25943  dvaddbr  26002  dvcobr  26010  dvcj  26014  dvfre  26015  dvcnvlem  26040  dvlip  26057  dvlipcn  26058  c1lip1  26061  tdeglem4  26122  tdeglem2  26123  coe1mul3  26161  ply1rem  26228  fta1g  26232  ig1pdvds  26242  plyf  26260  plyeq0lem  26272  plypf1  26274  plyaddlem  26277  plymullem  26278  plyco  26303  dgreq  26306  0dgrb  26308  coefv0  26310  coeaddlem  26311  coemullem  26312  coemulc  26317  plycn  26323  dgrcolem2  26336  plycjlem  26338  plycj  26339  plycjOLD  26341  plyrecj  26343  plyreres  26349  dvply1  26350  vieta1lem2  26377  vieta1  26378  elqaalem2  26386  aareccl  26392  aalioulem1  26398  ulmcaulem  26459  ulmcau  26460  ulmcn  26464  mtest  26469  psergf  26477  dvradcnv  26486  psercn2  26488  pserdvlem2  26493  pserdv2  26495  abelthlem6  26501  abelthlem8  26504  abelthlem9  26505  logtayl  26727  amgm  27057  ftalem1  27139  ftalem2  27140  ftalem3  27141  ftalem4  27142  ftalem5  27143  basellem2  27148  muinv  27259  dchrmulcl  27315  dchrinvcl  27319  dchrfi  27321  dchrghm  27322  dchrsum2  27334  dchrsum  27335  bposlem5  27354  lgscllem  27370  lgsval4a  27385  lgsneg  27387  lgsdir  27398  lgsdilem2  27399  lgsdi  27400  lgsne0  27401  lgseisenlem3  27443  rpvmasumlem  27553  dchrmusum2  27560  dchrvmasumiflem1  27567  dchrisum0ff  27573  dchrisum0flblem1  27574  dchrisum0fno1  27577  rpvmasum2  27578  dchrisum0re  27579  dchrisum0lem2a  27583  upgrreslem  29507  umgrreslem  29508  wlkpvtx  29860  wlkepvtx  29861  usgr2pthlem  29965  frgrncvvdeqlem8  30510  lnoadd  30963  lnosub  30964  nmosetre  30969  nmooge0  30972  nmoub3i  30978  nmounbi  30981  phoeqi  31062  ubthlem1  31075  h2hcau  31184  h2hlm  31185  hoscl  31950  homcl  31951  hodcl  31952  hoaddcl  31963  homulcl  31964  homullid  32005  homco1  32006  homulass  32007  hoadddi  32008  hoadddir  32009  hoeq1  32035  hoeq2  32036  adjsym  32038  nmopsetretALT  32068  nmfnsetre  32082  cnvadj  32097  hhcno  32109  hhcnf  32110  nmopub2tALT  32114  nmopge0  32116  unopf1o  32121  unoplin  32125  counop  32126  nmfnleub2  32131  nmfnge0  32132  hmoplin  32147  eigvalcl  32166  lnop0  32171  hmops  32225  hmopm  32226  nlelchi  32266  leop2  32329  leopadd  32337  leopmuli  32338  leopnmid  32343  hmopidmchi  32356  pjinvari  32396  sticl  32420  fcomptf  32862  rge0scvg  34248  esumcst  34362  esumfzf  34368  esumfsup  34369  esumfsupre  34370  hasheuni  34384  measdivcstALTV  34524  eulerpartlems  34659  eulerpartlemgc  34661  eulerpartlemb  34667  derangsn  35525  subfacp1lem5  35539  subfacp1lem6  35540  pconnconn  35586  sconnpi1  35594  txsconnlem  35595  cvxsconn  35598  cvmliftphtlem  35672  cvmlift3lem2  35675  cvmlift3lem4  35677  cvmlift3lem6  35679  satfvel  35767  satefvfmla1  35780  elmrsubrn  35875  msubff  35885  msubvrs  35915  mclsssvlem  35917  faclim  36101  curf  38102  uncf  38103  curunc  38106  unccur  38107  matunitlindflem1  38120  matunitlindflem2  38121  ptrecube  38124  heicant  38159  mblfinlem2  38162  itg2addnclem  38175  ftc1anclem1  38197  ftc1anclem2  38198  ftc1anclem4  38200  upixp  38233  fdc  38249  seqpo  38251  incsequz  38252  incsequz2  38253  metf1o  38259  geomcau  38263  sstotbnd2  38278  prdsbnd  38297  ismtyima  38307  ismtyhmeolem  38308  heiborlem3  38317  heiborlem6  38320  heiborlem10  38324  bfplem1  38326  ghomco  38395  sticksstones11  42778  mzpclall  43313  mzprename  43335  rexrabdioph  43376  rmydioph  43596  rmxdioph  43598  expdiophlem2  43604  expdioph  43605  pw2f1ocnv  43619  kelac1  43645  rngunsnply  43751  ofsubid  44905  ofdivrec  44907  ofdivcan4  44908  ofdivdiv2  44909  dvconstbi  44915  refsum2cnlem1  45622  climinf  46187  stoweidlem26  46605  stoweidlem60  46639  stoweid  46642  dmvolsal  46925  caratheodory  47107  elhoi  47121  smfresal  47367  f1oresf1o2  47890  fargshiftf  48051  nnsum4primeseven  48427  nnsum4primesevenALTV  48428  isubgrvtxuhgr  48491  isubgruhgr  48495  isubgr0uhgr  48500  grimuhgr  48514  gricushgr  48544  rmsupp0  48995  domnmsuppn0  48996  gsumlsscl  49007  lincfsuppcl  49040  linccl  49041  lincdifsn  49051  lincsum  49056  lincscm  49057  lincscmcl  49059  lincext1  49081  lindslinindimp2lem1  49085  lindslinindimp2lem4  49088  lindslinindsimp2lem5  49089  snlindsntor  49098  lincresunitlem2  49103  lincresunit3lem1  49106  lincresunit3lem2  49107  lincresunit3  49108  lincreslvec3  49109  isldepslvec2  49112  zlmodzxzldeplem3  49129  1arympt1  49265  ackendofnn0  49311  xpco2  49483  aacllem  50427