Theorem ffvelcdm 7070

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 6698	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fnfvelrn 7069	. . 3 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
3	1, 2	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ ran 𝐹)
4		frn 6706	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵)
5	4	sseld 3930	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
6	5	adantr 486	. 2 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → ((𝐹‘𝐶) ∈ ran 𝐹 → (𝐹‘𝐶) ∈ 𝐵))
7	3, 6	mpd 16	1 ⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145  ran crn 5649   Fn wfn 6523  ⟶wf 6524  ‘cfv 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2213  ax-ext 2732  ax-sep 5249  ax-nul 5260  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-iota 6484  df-fun 6530  df-fn 6531  df-f 6532  df-fv 6536

This theorem is used by:  ffvelcdmi  7072  ffvelcdmda  7073  dffo3  7091  dffo3f  7095  foco2  7098  ffnfv  7108  ffvresb  7115  fcompt  7123  fsn2  7126  fvconst  7156  fprb  7188  f1cofveqaeq  7250  fcofo  7285  cocan1  7288  fvf1pr  7304  isocnv  7327  isocnv3  7329  isores2  7330  isopolem  7342  isosolem  7344  fovcdm  7580  off  7695  fnwelem  8127  soseq  8155  smofvon2  8343  smocdmdom  8355  omsmolem  8645  omsmo  8646  fsetfcdm  8861  curf  8869  uncf  8870  mapfvd  8886  mapsncnv  8900  2dom  9037  xpdom2  9070  domunsncan  9075  xpmapenlem  9142  fiint  9296  infdifsn  9636  cantnflem1  9668  wemapwe  9676  cnfcom3lem  9682  updjudhf  9969  fseqenlem1  10060  finacn  10086  ackbij1lem12  10265  cofsmo  10304  cfsmolem  10305  cfcoflem  10307  coftr  10308  isf32lem6  10393  isf32lem7  10394  isf34lem7  10414  isf34lem6  10415  acncc  10475  axdc2lem  10483  axdc3lem2  10486  axdc3lem4  10488  axdc4lem  10490  axcclem  10492  ttukeylem6  10549  alephreg  10624  pwcfsdom  10625  canthp1lem2  10695  canthp1  10696  pwfseqlem1  10700  pwfseqlem4a  10703  gruf  10853  fsequb2  14073  axdc4uzlem  14080  seqf1o  14140  hashf1lem1  14553  wwlktovf  15062  shftf  15185  limsupgre  15601  rlimuni  15670  lo1resb  15684  o1resb  15686  o1of2  15733  o1rlimmul  15739  isercolllem1  15785  isercolllem2  15786  isercolllem3  15787  isercoll  15788  climsup  15790  iseralt  15805  sumeq2ii  15813  summolem2a  15834  isumcl  15880  isumshft  15961  climcndslem2  15972  climcnds  15973  mertenslem2  16007  prodeq2ii  16033  prodmolem2a  16054  iprodcl  16121  rpnnen2lem10  16344  ruclem8  16358  ruclem12  16362  3dvds  16454  smueqlem  16613  nn0seqcvgd  16693  algrf  16696  eucalg  16710  phimullem  16903  pcmpt  17017  pcprod  17020  vdwlem11  17116  vdwnnlem3  17122  ramlb  17144  0ram  17145  ramcl  17154  prmgaplem8  17183  imasaddfnlem  17647  imasaddflem  17649  chnpof1  18751  mgmhmpropd  18834  mhmpropd  18934  smndex1gid  19047  smndex1gidOLD  19048  ghmsub  19385  cntzmhm  19502  f1omvdconj  19607  pj1ghm  19864  gsumzaddlem  20082  gsumzadd  20083  gsummptnn0fzfv  20148  dprdfadd  20183  subgdmdprd  20197  gsumdixp  20495  lspcl  21198  znunit  21816  frlmsslsp  22049  frlmup2  22052  lindfmm  22080  islindf4  22091  psrbaglesupp  22177  psrbaglefi  22181  resspsrmul  22230  evlslem4  22332  evlslem3  22336  fvcoe1  22472  psropprmul  22502  00ply1bas  22504  subrgvr1cl  22528  coe1mul2lem1  22533  coe1tmmul  22543  ply1coe  22563  evl1val  22594  evl1sca  22599  pf1const  22611  1mavmul  22810  mavmulass  22811  marepvcl  22831  1marepvmarrepid  22837  matunitlindflem1  22941  matunitlindflem2  22942  cramerimplem1  22948  pmatcollpw3fi1lem1  23051  pmatcollpw3fi1lem2  23052  cpmadugsumlemF  23141  cpmadugsumfi  23142  cayleyhamilton1  23157  hauscmplem  23671  ptbasid  23841  ptpjcn  23877  upxp  23889  uptx  23891  txcmplem2  23908  xkopt  23921  txhmeo  24069  alexsubALTlem3  24315  nrginvrcn  24958  nmoi  24994  nmoleub  24997  cncfmet  25177  cnheibor  25223  evth  25227  pcopt  25290  pcopt2  25291  pcorevlem  25294  pi1xfrf  25321  pi1xfr  25323  pi1xfrcnvlem  25324  iscauf  25548  iscmet3lem1  25559  iscmet3lem2  25560  iscmet3  25561  causs  25566  bcthlem5  25596  bcth3  25599  ovolfcl  25734  ovolfioo  25735  ovolficc  25736  ovolficcss  25737  ovolfsval  25738  ovolmge0  25745  ovollb2lem  25756  ovolunlem1a  25764  ovoliunlem1  25770  ovoliunlem2  25771  ovoliun  25773  ovolicc1  25784  ovolicc2lem3  25787  ovolicc2lem4  25788  ovolicc2lem5  25789  voliunlem1  25818  volsup  25824  ioombl1lem2  25827  ovolfs2  25839  uniioovol  25847  uniiccvol  25848  uniioombllem3a  25852  uniioombllem3  25853  uniioombllem4  25854  uniioombllem5  25855  uniioombllem6  25856  dyadmbl  25868  volcn  25874  ismbf  25896  mbfadd  25929  mbfsub  25930  mbflimsup  25934  0plef  25940  itg1climres  25982  mbfi1fseqlem1  25983  mbfi1fseqlem3  25985  mbfi1fseqlem4  25986  mbfi1fseqlem5  25987  mbfmul  25994  xrge0f  25999  itg2ge0  26003  itg2seq  26010  itg2uba  26011  itg2lea  26012  itg2eqa  26013  itg2splitlem  26016  itg2split  26017  itg2i1fseqle  26022  itg2i1fseq  26023  itg2i1fseq2  26024  itg2addlem  26026  bddmulibl  26106  ellimc3  26146  dvaddbr  26205  dvcobr  26213  dvcj  26217  dvfre  26218  dvcnvlem  26243  dvlip  26260  dvlipcn  26261  c1lip1  26264  tdeglem4  26325  tdeglem2  26326  coe1mul3  26364  ply1rem  26431  fta1g  26435  ig1pdvds  26445  plyf  26463  plyeq0lem  26476  plypf1  26478  plyaddlem  26481  plymullem  26482  plyco  26507  dgreq  26510  0dgrb  26512  coefv0  26514  coeaddlem  26515  coemullem  26516  coemulc  26521  plycn  26527  dgrcolem2  26540  plycjlem  26542  plycj  26543  plycjOLD  26545  plyrecj  26547  plyreres  26553  dvply1  26554  vieta1lem2  26583  vieta1  26584  elqaalem2  26592  aareccl  26602  aalioulem1  26608  ulmcaulem  26670  ulmcau  26671  ulmcn  26675  mtest  26680  psergf  26688  dvradcnv  26697  psercn2  26699  pserdvlem2  26704  pserdv2  26706  abelthlem6  26712  abelthlem8  26715  abelthlem9  26716  logtayl  26937  amgm  27267  ftalem1  27349  ftalem2  27350  ftalem3  27351  ftalem4  27352  ftalem5  27353  basellem2  27358  muinv  27469  dchrmulcl  27525  dchrinvcl  27529  dchrfi  27531  dchrghm  27532  dchrsum2  27544  dchrsum  27545  bposlem5  27564  lgscllem  27580  lgsval4a  27595  lgsneg  27597  lgsdir  27608  lgsdilem2  27609  lgsdi  27610  lgsne0  27611  lgseisenlem3  27653  rpvmasumlem  27763  dchrmusum2  27770  dchrvmasumiflem1  27777  dchrisum0ff  27783  dchrisum0flblem1  27784  dchrisum0fno1  27787  rpvmasum2  27788  dchrisum0re  27789  dchrisum0lem2a  27793  upgrreslem  29804  umgrreslem  29805  wlkpvtx  30157  wlkepvtx  30158  usgr2pthlem  30268  frgrncvvdeqlem8  30826  lnoadd  31279  lnosub  31280  nmosetre  31285  nmooge0  31288  nmoub3i  31294  nmounbi  31297  phoeqi  31378  ubthlem1  31391  h2hcau  31500  h2hlm  31501  hoscl  32266  homcl  32267  hodcl  32268  hoaddcl  32279  homulcl  32280  homullid  32321  homco1  32322  homulass  32323  hoadddi  32324  hoadddir  32325  hoeq1  32351  hoeq2  32352  adjsym  32354  nmopsetretALT  32384  nmfnsetre  32398  cnvadj  32413  hhcno  32425  hhcnf  32426  nmopub2tALT  32430  nmopge0  32432  unopf1o  32437  unoplin  32441  counop  32442  nmfnleub2  32447  nmfnge0  32448  hmoplin  32463  eigvalcl  32482  lnop0  32487  hmops  32541  hmopm  32542  nlelchi  32582  leop2  32645  leopadd  32653  leopmuli  32654  leopnmid  32659  hmopidmchi  32672  pjinvari  32712  sticl  32736  fcomptf  33171  rge0scvg  34500  esumcst  34614  esumfzf  34620  esumfsup  34621  esumfsupre  34622  hasheuni  34636  measdivcstALTV  34777  eulerpartlems  34912  eulerpartlemgc  34914  eulerpartlemb  34920  derangsn  35850  subfacp1lem5  35864  subfacp1lem6  35865  pconnconn  35911  sconnpi1  35919  txsconnlem  35920  cvxsconn  35923  cvmliftphtlem  35997  cvmlift3lem2  36000  cvmlift3lem4  36002  cvmlift3lem6  36004  satfvel  36092  satefvfmla1  36105  elmrsubrn  36200  msubff  36210  msubvrs  36240  mclsssvlem  36242  faclim  36426  curunc  38439  unccur  38440  ptrecube  38452  heicant  38487  mblfinlem2  38490  itg2addnclem  38503  ftc1anclem1  38525  ftc1anclem2  38526  ftc1anclem4  38528  upixp  38577  fdc  38593  seqpo  38595  incsequz  38596  incsequz2  38597  metf1o  38603  geomcau  38607  sstotbnd2  38622  prdsbnd  38641  ismtyima  38651  ismtyhmeolem  38652  heiborlem3  38661  heiborlem6  38664  heiborlem10  38668  bfplem1  38670  ghomco  38739  sticksstones11  43120  mzpclall  43670  mzprename  43692  rexrabdioph  43733  rmydioph  43953  rmxdioph  43955  expdiophlem2  43961  expdioph  43962  pw2f1ocnv  43976  kelac1  44002  rngunsnply  44108  ofsubid  45246  ofdivrec  45248  ofdivcan4  45249  ofdivdiv2  45250  dvconstbi  45256  refsum2cnlem1  45969  climinf  46534  stoweidlem26  46952  stoweidlem60  46986  stoweid  46989  dmvolsal  47272  caratheodory  47454  elhoi  47468  smfresal  47714  sqrtrrnpoly  47858  f1oresf1o2  48277  fargshiftf  48438  nnsum4primeseven  48814  nnsum4primesevenALTV  48815  isubgrvtxuhgr  48878  isubgruhgr  48882  isubgr0uhgr  48887  grimuhgr  48901  gricushgr  48931  rmsupp0  49396  domnmsuppn0  49397  gsumlsscl  49408  lincfsuppcl  49441  linccl  49442  lincdifsn  49452  lincsum  49457  lincscm  49458  lincscmcl  49460  lincext1  49482  lindslinindimp2lem1  49486  lindslinindimp2lem4  49489  lindslinindsimp2lem5  49490  snlindsntor  49499  lincresunitlem2  49504  lincresunit3lem1  49507  lincresunit3lem2  49508  lincresunit3  49509  lincreslvec3  49510  isldepslvec2  49513  zlmodzxzldeplem3  49530  1arympt1  49666  ackendofnn0  49712  xpco2  49883  aacllem  50855