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 6705	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7075	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 591	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6713	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3935	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 485	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 16	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∈ wcel 2142  ran crn 5661   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is used by:  ffvelcdmi  7078  ffvelcdmda  7079  dffo3  7097  dffo3f  7101  foco2  7104  ffnfv  7114  ffvresb  7121  fcompt  7129  fsn2  7132  fvconst  7160  fprb  7192  f1cofveqaeq  7255  fcofo  7286  cocan1  7289  fvf1pr  7305  isocnv  7328  isocnv3  7330  isores2  7331  isopolem  7343  isosolem  7345  fovcdm  7582  off  7694  fnwelem  8125  soseq  8153  smofvon2  8341  smocdmdom  8353  omsmolem  8641  omsmo  8642  fsetfcdm  8855  mapfvd  8875  mapsncnv  8889  2dom  9025  xpdom2  9058  domunsncan  9063  xpmapenlem  9130  fiint  9284  infdifsn  9624  cantnflem1  9656  wemapwe  9664  cnfcom3lem  9670  updjudhf  9924  fseqenlem1  10015  finacn  10041  ackbij1lem12  10220  cofsmo  10259  cfsmolem  10260  cfcoflem  10262  coftr  10263  isf32lem6  10348  isf32lem7  10349  isf34lem7  10369  isf34lem6  10370  acncc  10430  axdc2lem  10438  axdc3lem2  10441  axdc3lem4  10443  axdc4lem  10445  axcclem  10447  ttukeylem6  10504  alephreg  10573  pwcfsdom  10574  canthp1lem2  10644  canthp1  10645  pwfseqlem1  10649  pwfseqlem4a  10652  gruf  10802  fsequb2  14019  axdc4uzlem  14026  seqf1o  14086  hashf1lem1  14499  wwlktovf  15000  shftf  15123  limsupgre  15539  rlimuni  15608  lo1resb  15622  o1resb  15624  o1of2  15671  o1rlimmul  15677  isercolllem1  15723  isercolllem2  15724  isercolllem3  15725  isercoll  15726  climsup  15728  iseralt  15743  sumeq2ii  15751  summolem2a  15773  isumcl  15819  isumshft  15900  climcndslem2  15911  climcnds  15912  mertenslem2  15946  prodeq2ii  15972  prodmolem2a  15995  iprodcl  16062  rpnnen2lem10  16285  ruclem8  16299  ruclem12  16303  3dvds  16395  smueqlem  16554  nn0seqcvgd  16634  algrf  16637  eucalg  16651  phimullem  16844  pcmpt  16958  pcprod  16961  vdwlem11  17057  vdwnnlem3  17063  ramlb  17085  0ram  17086  ramcl  17095  prmgaplem8  17124  imasaddfnlem  17588  imasaddflem  17590  chnpof1  18692  mgmhmpropd  18762  mhmpropd  18856  smndex1gid  18969  smndex1gidOLD  18970  ghmsub  19300  cntzmhm  19417  f1omvdconj  19522  pj1ghm  19779  gsumzaddlem  19997  gsumzadd  19998  gsummptnn0fzfv  20063  dprdfadd  20098  subgdmdprd  20112  gsumdixp  20407  lspcl  21108  znunit  21724  frlmsslsp  21957  frlmup2  21960  lindfmm  21988  islindf4  21999  psrbaglesupp  22083  psrbaglefi  22087  resspsrmul  22136  evlslem4  22238  evlslem3  22242  fvcoe1  22378  psropprmul  22408  00ply1bas  22410  subrgvr1cl  22434  coe1mul2lem1  22439  coe1tmmul  22449  ply1coe  22469  evl1val  22500  evl1sca  22505  pf1const  22517  1mavmul  22716  mavmulass  22717  marepvcl  22737  1marepvmarrepid  22743  cramerimplem1  22851  pmatcollpw3fi1lem1  22954  pmatcollpw3fi1lem2  22955  cpmadugsumlemF  23044  cpmadugsumfi  23045  cayleyhamilton1  23060  hauscmplem  23574  ptbasid  23743  ptpjcn  23779  upxp  23791  uptx  23793  txcmplem2  23810  xkopt  23823  txhmeo  23971  alexsubALTlem3  24217  nrginvrcn  24860  nmoi  24896  nmoleub  24899  cncfmet  25079  cnheibor  25125  evth  25129  pcopt  25192  pcopt2  25193  pcorevlem  25196  pi1xfrf  25223  pi1xfr  25225  pi1xfrcnvlem  25226  iscauf  25450  iscmet3lem1  25461  iscmet3lem2  25462  iscmet3  25463  causs  25468  bcthlem5  25498  bcth3  25501  ovolfcl  25636  ovolfioo  25637  ovolficc  25638  ovolficcss  25639  ovolfsval  25640  ovolmge0  25647  ovollb2lem  25658  ovolunlem1a  25666  ovoliunlem1  25672  ovoliunlem2  25673  ovoliun  25675  ovolicc1  25686  ovolicc2lem3  25689  ovolicc2lem4  25690  ovolicc2lem5  25691  voliunlem1  25720  volsup  25726  ioombl1lem2  25729  ovolfs2  25741  uniioovol  25749  uniiccvol  25750  uniioombllem3a  25754  uniioombllem3  25755  uniioombllem4  25756  uniioombllem5  25757  uniioombllem6  25758  dyadmbl  25770  volcn  25776  ismbf  25798  mbfadd  25831  mbfsub  25832  mbflimsup  25836  0plef  25842  itg1climres  25884  mbfi1fseqlem1  25885  mbfi1fseqlem3  25887  mbfi1fseqlem4  25888  mbfi1fseqlem5  25889  mbfmul  25896  xrge0f  25901  itg2ge0  25905  itg2seq  25912  itg2uba  25913  itg2lea  25914  itg2eqa  25915  itg2splitlem  25918  itg2split  25919  itg2i1fseqle  25924  itg2i1fseq  25925  itg2i1fseq2  25926  itg2addlem  25928  bddmulibl  26009  ellimc3  26049  dvaddbr  26108  dvcobr  26116  dvcj  26120  dvfre  26121  dvcnvlem  26146  dvlip  26163  dvlipcn  26164  c1lip1  26167  tdeglem4  26228  tdeglem2  26229  coe1mul3  26267  ply1rem  26334  fta1g  26338  ig1pdvds  26348  plyf  26366  plyeq0lem  26378  plypf1  26380  plyaddlem  26383  plymullem  26384  plyco  26409  dgreq  26412  0dgrb  26414  coefv0  26416  coeaddlem  26417  coemullem  26418  coemulc  26423  plycn  26429  dgrcolem2  26442  plycjlem  26444  plycj  26445  plycjOLD  26447  plyrecj  26449  plyreres  26455  dvply1  26456  vieta1lem2  26483  vieta1  26484  elqaalem2  26492  aareccl  26500  aalioulem1  26506  ulmcaulem  26568  ulmcau  26569  ulmcn  26573  mtest  26578  psergf  26586  dvradcnv  26595  psercn2  26597  pserdvlem2  26602  pserdv2  26604  abelthlem6  26610  abelthlem8  26613  abelthlem9  26614  logtayl  26836  amgm  27166  ftalem1  27248  ftalem2  27249  ftalem3  27250  ftalem4  27251  ftalem5  27252  basellem2  27257  muinv  27368  dchrmulcl  27424  dchrinvcl  27428  dchrfi  27430  dchrghm  27431  dchrsum2  27443  dchrsum  27444  bposlem5  27463  lgscllem  27479  lgsval4a  27494  lgsneg  27496  lgsdir  27507  lgsdilem2  27508  lgsdi  27509  lgsne0  27510  lgseisenlem3  27552  rpvmasumlem  27662  dchrmusum2  27669  dchrvmasumiflem1  27676  dchrisum0ff  27682  dchrisum0flblem1  27683  dchrisum0fno1  27686  rpvmasum2  27687  dchrisum0re  27688  dchrisum0lem2a  27692  upgrreslem  29665  umgrreslem  29666  wlkpvtx  30018  wlkepvtx  30019  usgr2pthlem  30123  frgrncvvdeqlem8  30668  lnoadd  31121  lnosub  31122  nmosetre  31127  nmooge0  31130  nmoub3i  31136  nmounbi  31139  phoeqi  31220  ubthlem1  31233  h2hcau  31342  h2hlm  31343  hoscl  32108  homcl  32109  hodcl  32110  hoaddcl  32121  homulcl  32122  homullid  32163  homco1  32164  homulass  32165  hoadddi  32166  hoadddir  32167  hoeq1  32193  hoeq2  32194  adjsym  32196  nmopsetretALT  32226  nmfnsetre  32240  cnvadj  32255  hhcno  32267  hhcnf  32268  nmopub2tALT  32272  nmopge0  32274  unopf1o  32279  unoplin  32283  counop  32284  nmfnleub2  32289  nmfnge0  32290  hmoplin  32305  eigvalcl  32324  lnop0  32329  hmops  32383  hmopm  32384  nlelchi  32424  leop2  32487  leopadd  32495  leopmuli  32496  leopnmid  32501  hmopidmchi  32514  pjinvari  32554  sticl  32578  fcomptf  33014  rge0scvg  34348  esumcst  34462  esumfzf  34468  esumfsup  34469  esumfsupre  34470  hasheuni  34484  measdivcstALTV  34624  eulerpartlems  34759  eulerpartlemgc  34761  eulerpartlemb  34767  derangsn  35670  subfacp1lem5  35684  subfacp1lem6  35685  pconnconn  35731  sconnpi1  35739  txsconnlem  35740  cvxsconn  35743  cvmliftphtlem  35817  cvmlift3lem2  35820  cvmlift3lem4  35822  cvmlift3lem6  35824  satfvel  35912  satefvfmla1  35925  elmrsubrn  36020  msubff  36030  msubvrs  36060  mclsssvlem  36062  faclim  36246  curf  38277  uncf  38278  curunc  38281  unccur  38282  matunitlindflem1  38295  matunitlindflem2  38296  ptrecube  38299  heicant  38334  mblfinlem2  38337  itg2addnclem  38350  ftc1anclem1  38372  ftc1anclem2  38373  ftc1anclem4  38375  upixp  38408  fdc  38424  seqpo  38426  incsequz  38427  incsequz2  38428  metf1o  38434  geomcau  38438  sstotbnd2  38453  prdsbnd  38472  ismtyima  38482  ismtyhmeolem  38483  heiborlem3  38492  heiborlem6  38495  heiborlem10  38499  bfplem1  38501  ghomco  38570  sticksstones11  42951  mzpclall  43486  mzprename  43508  rexrabdioph  43549  rmydioph  43769  rmxdioph  43771  expdiophlem2  43777  expdioph  43778  pw2f1ocnv  43792  kelac1  43818  rngunsnply  43924  ofsubid  45062  ofdivrec  45064  ofdivcan4  45065  ofdivdiv2  45066  dvconstbi  45072  refsum2cnlem1  45785  climinf  46350  stoweidlem26  46768  stoweidlem60  46802  stoweid  46805  dmvolsal  47088  caratheodory  47270  elhoi  47284  smfresal  47530  f1oresf1o2  48056  fargshiftf  48217  nnsum4primeseven  48593  nnsum4primesevenALTV  48594  isubgrvtxuhgr  48657  isubgruhgr  48661  isubgr0uhgr  48666  grimuhgr  48680  gricushgr  48710  rmsupp0  49176  domnmsuppn0  49177  gsumlsscl  49188  lincfsuppcl  49221  linccl  49222  lincdifsn  49232  lincsum  49237  lincscm  49238  lincscmcl  49240  lincext1  49262  lindslinindimp2lem1  49266  lindslinindimp2lem4  49269  lindslinindsimp2lem5  49270  snlindsntor  49279  lincresunitlem2  49284  lincresunit3lem1  49287  lincresunit3lem2  49288  lincresunit3  49289  lincreslvec3  49290  isldepslvec2  49293  zlmodzxzldeplem3  49310  1arympt1  49446  ackendofnn0  49492  xpco2  49663  aacllem  50649