Theorem ffvelcdm 7014

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ran crn 5615   Fn wfn 6476  ⟶wf 6477  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-fv 6489

This theorem is referenced by:  ffvelcdmi  7016  ffvelcdmda  7017  dffo3  7035  dffo3f  7039  foco2  7042  ffnfv  7052  ffvresb  7058  fcompt  7066  fsn2  7069  fvconst  7096  fprb  7128  f1cofveqaeq  7191  fcofo  7222  cocan1  7225  fvf1pr  7241  isocnv  7264  isocnv3  7266  isores2  7267  isopolem  7279  isosolem  7281  fovcdm  7516  off  7628  fnwelem  8061  soseq  8089  smofvon2  8276  smocdmdom  8288  omsmolem  8572  omsmo  8573  fsetfcdm  8784  mapfvd  8803  mapsncnv  8817  2dom  8952  xpdom2  8985  domunsncan  8990  xpmapenlem  9057  fiint  9211  infdifsn  9547  cantnflem1  9579  wemapwe  9587  cnfcom3lem  9593  updjudhf  9824  fseqenlem1  9915  finacn  9941  ackbij1lem12  10121  cofsmo  10160  cfsmolem  10161  cfcoflem  10163  coftr  10164  isf32lem6  10249  isf32lem7  10250  isf34lem7  10270  isf34lem6  10271  acncc  10331  axdc2lem  10339  axdc3lem2  10342  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  ttukeylem6  10405  alephreg  10473  pwcfsdom  10474  canthp1lem2  10544  canthp1  10545  pwfseqlem1  10549  pwfseqlem4a  10552  gruf  10702  fsequb2  13883  axdc4uzlem  13890  seqf1o  13950  hashf1lem1  14362  wwlktovf  14863  shftf  14986  limsupgre  15388  rlimuni  15457  lo1resb  15471  o1resb  15473  o1of2  15520  o1rlimmul  15526  isercolllem1  15572  isercolllem2  15573  isercolllem3  15574  isercoll  15575  climsup  15577  iseralt  15592  sumeq2ii  15600  summolem2a  15622  isumcl  15668  isumshft  15746  climcndslem2  15757  climcnds  15758  mertenslem2  15792  prodeq2ii  15818  prodmolem2a  15841  iprodcl  15908  rpnnen2lem10  16132  ruclem8  16146  ruclem12  16150  3dvds  16242  smueqlem  16401  nn0seqcvgd  16481  algrf  16484  eucalg  16498  phimullem  16690  pcmpt  16804  pcprod  16807  vdwlem11  16903  vdwnnlem3  16909  ramlb  16931  0ram  16932  ramcl  16941  prmgaplem8  16970  imasaddfnlem  17432  imasaddflem  17434  chnpof1  18536  mgmhmpropd  18606  mhmpropd  18700  smndex1gid  18811  ghmsub  19136  cntzmhm  19253  f1omvdconj  19358  pj1ghm  19615  gsumzaddlem  19833  gsumzadd  19834  gsummptnn0fzfv  19899  dprdfadd  19934  subgdmdprd  19948  gsumdixp  20237  lspcl  20909  znunit  21500  frlmsslsp  21733  frlmup2  21736  lindfmm  21764  islindf4  21775  psrbaglesupp  21859  psrbaglefi  21863  resspsrmul  21913  evlslem4  22011  evlslem3  22015  fvcoe1  22120  psropprmul  22150  00ply1bas  22152  subrgvr1cl  22176  coe1mul2lem1  22181  coe1tmmul  22191  ply1coe  22213  evl1val  22244  evl1sca  22249  pf1const  22261  1mavmul  22463  mavmulass  22464  marepvcl  22484  1marepvmarrepid  22490  cramerimplem1  22598  pmatcollpw3fi1lem1  22701  pmatcollpw3fi1lem2  22702  cpmadugsumlemF  22791  cpmadugsumfi  22792  cayleyhamilton1  22807  hauscmplem  23321  ptbasid  23490  ptpjcn  23526  upxp  23538  uptx  23540  txcmplem2  23557  xkopt  23570  txhmeo  23718  alexsubALTlem3  23964  nrginvrcn  24607  nmoi  24643  nmoleub  24646  cncfmet  24829  cnheibor  24881  evth  24885  pcopt  24949  pcopt2  24950  pcorevlem  24953  pi1xfrf  24980  pi1xfr  24982  pi1xfrcnvlem  24983  iscauf  25207  iscmet3lem1  25218  iscmet3lem2  25219  iscmet3  25220  causs  25225  bcthlem5  25255  bcth3  25258  ovolfcl  25394  ovolfioo  25395  ovolficc  25396  ovolficcss  25397  ovolfsval  25398  ovolmge0  25405  ovollb2lem  25416  ovolunlem1a  25424  ovoliunlem1  25430  ovoliunlem2  25431  ovoliun  25433  ovolicc1  25444  ovolicc2lem3  25447  ovolicc2lem4  25448  ovolicc2lem5  25449  voliunlem1  25478  volsup  25484  ioombl1lem2  25487  ovolfs2  25499  uniioovol  25507  uniiccvol  25508  uniioombllem3a  25512  uniioombllem3  25513  uniioombllem4  25514  uniioombllem5  25515  uniioombllem6  25516  dyadmbl  25528  volcn  25534  ismbf  25556  mbfadd  25589  mbfsub  25590  mbflimsup  25594  0plef  25600  itg1climres  25642  mbfi1fseqlem1  25643  mbfi1fseqlem3  25645  mbfi1fseqlem4  25646  mbfi1fseqlem5  25647  mbfmul  25654  xrge0f  25659  itg2ge0  25663  itg2seq  25670  itg2uba  25671  itg2lea  25672  itg2eqa  25673  itg2splitlem  25676  itg2split  25677  itg2i1fseqle  25682  itg2i1fseq  25683  itg2i1fseq2  25684  itg2addlem  25686  bddmulibl  25767  ellimc3  25807  dvaddbr  25867  dvcobr  25876  dvcobrOLD  25877  dvcj  25881  dvfre  25882  dvcnvlem  25907  dvlip  25925  dvlipcn  25926  c1lip1  25929  tdeglem4  25992  tdeglem2  25993  coe1mul3  26031  ply1rem  26098  fta1g  26102  ig1pdvds  26112  plyf  26130  plyeq0lem  26142  plypf1  26144  plyaddlem  26147  plymullem  26148  plyco  26173  dgreq  26176  0dgrb  26178  coefv0  26180  coeaddlem  26181  coemullem  26182  coemulc  26187  plycn  26193  plycnOLD  26194  dgrcolem2  26207  plycjlem  26209  plycj  26210  plycjOLD  26212  plyrecj  26214  plyreres  26217  dvply1  26218  vieta1lem2  26246  vieta1  26247  elqaalem2  26255  aareccl  26261  aalioulem1  26267  ulmcaulem  26330  ulmcau  26331  ulmcn  26335  mtest  26340  psergf  26348  dvradcnv  26357  psercn2  26359  psercn2OLD  26360  pserdvlem2  26365  pserdv2  26367  abelthlem6  26373  abelthlem8  26376  abelthlem9  26377  logtayl  26596  amgm  26928  ftalem1  27010  ftalem2  27011  ftalem3  27012  ftalem4  27013  ftalem5  27014  basellem2  27019  muinv  27130  dchrmulcl  27187  dchrinvcl  27191  dchrfi  27193  dchrghm  27194  dchrsum2  27206  dchrsum  27207  bposlem5  27226  lgscllem  27242  lgsval4a  27257  lgsneg  27259  lgsdir  27270  lgsdilem2  27271  lgsdi  27272  lgsne0  27273  lgseisenlem3  27315  rpvmasumlem  27425  dchrmusum2  27432  dchrvmasumiflem1  27439  dchrisum0ff  27445  dchrisum0flblem1  27446  dchrisum0fno1  27449  rpvmasum2  27450  dchrisum0re  27451  dchrisum0lem2a  27455  upgrreslem  29282  umgrreslem  29283  wlkpvtx  29636  wlkepvtx  29637  usgr2pthlem  29741  frgrncvvdeqlem8  30286  lnoadd  30738  lnosub  30739  nmosetre  30744  nmooge0  30747  nmoub3i  30753  nmounbi  30756  phoeqi  30837  ubthlem1  30850  h2hcau  30959  h2hlm  30960  hoscl  31725  homcl  31726  hodcl  31727  hoaddcl  31738  homulcl  31739  homullid  31780  homco1  31781  homulass  31782  hoadddi  31783  hoadddir  31784  hoeq1  31810  hoeq2  31811  adjsym  31813  nmopsetretALT  31843  nmfnsetre  31857  cnvadj  31872  hhcno  31884  hhcnf  31885  nmopub2tALT  31889  nmopge0  31891  unopf1o  31896  unoplin  31900  counop  31901  nmfnleub2  31906  nmfnge0  31907  hmoplin  31922  eigvalcl  31941  lnop0  31946  hmops  32000  hmopm  32001  nlelchi  32041  leop2  32104  leopadd  32112  leopmuli  32113  leopnmid  32118  hmopidmchi  32131  pjinvari  32171  sticl  32195  fcomptf  32640  rge0scvg  33962  esumcst  34076  esumfzf  34082  esumfsup  34083  esumfsupre  34084  hasheuni  34098  measdivcstALTV  34238  eulerpartlems  34373  eulerpartlemgc  34375  eulerpartlemb  34381  derangsn  35214  subfacp1lem5  35228  subfacp1lem6  35229  pconnconn  35275  sconnpi1  35283  txsconnlem  35284  cvxsconn  35287  cvmliftphtlem  35361  cvmlift3lem2  35364  cvmlift3lem4  35366  cvmlift3lem6  35368  satfvel  35456  satefvfmla1  35469  elmrsubrn  35564  msubff  35574  msubvrs  35604  mclsssvlem  35606  faclim  35790  curf  37648  uncf  37649  curunc  37652  unccur  37653  matunitlindflem1  37666  matunitlindflem2  37667  ptrecube  37670  heicant  37705  mblfinlem2  37708  itg2addnclem  37721  ftc1anclem1  37743  ftc1anclem2  37744  ftc1anclem4  37746  upixp  37779  fdc  37795  seqpo  37797  incsequz  37798  incsequz2  37799  metf1o  37805  geomcau  37809  sstotbnd2  37824  prdsbnd  37843  ismtyima  37853  ismtyhmeolem  37854  heiborlem3  37863  heiborlem6  37866  heiborlem10  37870  bfplem1  37872  ghomco  37941  sticksstones11  42259  mzpclall  42830  mzprename  42852  rexrabdioph  42897  rmydioph  43117  rmxdioph  43119  expdiophlem2  43125  expdioph  43126  pw2f1ocnv  43140  kelac1  43166  rngunsnply  43272  ofsubid  44427  ofdivrec  44429  ofdivcan4  44430  ofdivdiv2  44431  dvconstbi  44437  refsum2cnlem1  45144  climinf  45716  stoweidlem26  46134  stoweidlem60  46168  stoweid  46171  dmvolsal  46454  caratheodory  46636  elhoi  46650  smfresal  46896  f1oresf1o2  47401  fargshiftf  47550  nnsum4primeseven  47910  nnsum4primesevenALTV  47911  isubgrvtxuhgr  47974  isubgruhgr  47978  isubgr0uhgr  47983  grimuhgr  47997  gricushgr  48027  rmsupp0  48478  domnmsuppn0  48479  gsumlsscl  48490  lincfsuppcl  48524  linccl  48525  lincdifsn  48535  lincsum  48540  lincscm  48541  lincscmcl  48543  lincext1  48565  lindslinindimp2lem1  48569  lindslinindimp2lem4  48572  lindslinindsimp2lem5  48573  snlindsntor  48582  lincresunitlem2  48587  lincresunit3lem1  48590  lincresunit3lem2  48591  lincresunit3  48592  lincreslvec3  48593  isldepslvec2  48596  zlmodzxzldeplem3  48613  1arympt1  48749  ackendofnn0  48795  xpco2  48967  aacllem  49912