Theorem ffvelcdm 7035

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ran crn 5632   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507

This theorem is referenced by:  ffvelcdmi  7037  ffvelcdmda  7038  dffo3  7056  dffo3f  7060  foco2  7063  ffnfv  7073  ffvresb  7079  fcompt  7087  fsn2  7090  fvconst  7118  fprb  7150  f1cofveqaeq  7214  fcofo  7245  cocan1  7248  fvf1pr  7264  isocnv  7287  isocnv3  7289  isores2  7290  isopolem  7302  isosolem  7304  fovcdm  7539  off  7651  fnwelem  8087  soseq  8115  smofvon2  8302  smocdmdom  8314  omsmolem  8598  omsmo  8599  fsetfcdm  8810  mapfvd  8829  mapsncnv  8843  2dom  8978  xpdom2  9013  domunsncan  9018  xpmapenlem  9085  fiint  9253  fiintOLD  9254  infdifsn  9586  cantnflem1  9618  wemapwe  9626  cnfcom3lem  9632  updjudhf  9860  fseqenlem1  9953  finacn  9979  ackbij1lem12  10159  cofsmo  10198  cfsmolem  10199  cfcoflem  10201  coftr  10202  isf32lem6  10287  isf32lem7  10288  isf34lem7  10308  isf34lem6  10309  acncc  10369  axdc2lem  10377  axdc3lem2  10380  axdc3lem4  10382  axdc4lem  10384  axcclem  10386  ttukeylem6  10443  alephreg  10511  pwcfsdom  10512  canthp1lem2  10582  canthp1  10583  pwfseqlem1  10587  pwfseqlem4a  10590  gruf  10740  fsequb2  13917  axdc4uzlem  13924  seqf1o  13984  hashf1lem1  14396  wwlktovf  14898  shftf  15021  limsupgre  15423  rlimuni  15492  lo1resb  15506  o1resb  15508  o1of2  15555  o1rlimmul  15561  isercolllem1  15607  isercolllem2  15608  isercolllem3  15609  isercoll  15610  climsup  15612  iseralt  15627  sumeq2ii  15635  summolem2a  15657  isumcl  15703  isumshft  15781  climcndslem2  15792  climcnds  15793  mertenslem2  15827  prodeq2ii  15853  prodmolem2a  15876  iprodcl  15943  rpnnen2lem10  16167  ruclem8  16181  ruclem12  16185  3dvds  16277  smueqlem  16436  nn0seqcvgd  16516  algrf  16519  eucalg  16533  phimullem  16725  pcmpt  16839  pcprod  16842  vdwlem11  16938  vdwnnlem3  16944  ramlb  16966  0ram  16967  ramcl  16976  prmgaplem8  17005  imasaddfnlem  17467  imasaddflem  17469  mgmhmpropd  18607  mhmpropd  18701  smndex1gid  18812  ghmsub  19138  cntzmhm  19255  f1omvdconj  19360  pj1ghm  19617  gsumzaddlem  19835  gsumzadd  19836  gsummptnn0fzfv  19901  dprdfadd  19936  subgdmdprd  19950  gsumdixp  20239  lspcl  20914  znunit  21505  frlmsslsp  21738  frlmup2  21741  lindfmm  21769  islindf4  21780  psrbaglesupp  21864  psrbaglefi  21868  resspsrmul  21918  evlslem4  22016  evlslem3  22020  fvcoe1  22125  psropprmul  22155  00ply1bas  22157  subrgvr1cl  22181  coe1mul2lem1  22186  coe1tmmul  22196  ply1coe  22218  evl1val  22249  evl1sca  22254  pf1const  22266  1mavmul  22468  mavmulass  22469  marepvcl  22489  1marepvmarrepid  22495  cramerimplem1  22603  pmatcollpw3fi1lem1  22706  pmatcollpw3fi1lem2  22707  cpmadugsumlemF  22796  cpmadugsumfi  22797  cayleyhamilton1  22812  hauscmplem  23326  ptbasid  23495  ptpjcn  23531  upxp  23543  uptx  23545  txcmplem2  23562  xkopt  23575  txhmeo  23723  alexsubALTlem3  23969  nrginvrcn  24613  nmoi  24649  nmoleub  24652  cncfmet  24835  cnheibor  24887  evth  24891  pcopt  24955  pcopt2  24956  pcorevlem  24959  pi1xfrf  24986  pi1xfr  24988  pi1xfrcnvlem  24989  iscauf  25213  iscmet3lem1  25224  iscmet3lem2  25225  iscmet3  25226  causs  25231  bcthlem5  25261  bcth3  25264  ovolfcl  25400  ovolfioo  25401  ovolficc  25402  ovolficcss  25403  ovolfsval  25404  ovolmge0  25411  ovollb2lem  25422  ovolunlem1a  25430  ovoliunlem1  25436  ovoliunlem2  25437  ovoliun  25439  ovolicc1  25450  ovolicc2lem3  25453  ovolicc2lem4  25454  ovolicc2lem5  25455  voliunlem1  25484  volsup  25490  ioombl1lem2  25493  ovolfs2  25505  uniioovol  25513  uniiccvol  25514  uniioombllem3a  25518  uniioombllem3  25519  uniioombllem4  25520  uniioombllem5  25521  uniioombllem6  25522  dyadmbl  25534  volcn  25540  ismbf  25562  mbfadd  25595  mbfsub  25596  mbflimsup  25600  0plef  25606  itg1climres  25648  mbfi1fseqlem1  25649  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  mbfmul  25660  xrge0f  25665  itg2ge0  25669  itg2seq  25676  itg2uba  25677  itg2lea  25678  itg2eqa  25679  itg2splitlem  25682  itg2split  25683  itg2i1fseqle  25688  itg2i1fseq  25689  itg2i1fseq2  25690  itg2addlem  25692  bddmulibl  25773  ellimc3  25813  dvaddbr  25873  dvcobr  25882  dvcobrOLD  25883  dvcj  25887  dvfre  25888  dvcnvlem  25913  dvlip  25931  dvlipcn  25932  c1lip1  25935  tdeglem4  25998  tdeglem2  25999  coe1mul3  26037  ply1rem  26104  fta1g  26108  ig1pdvds  26118  plyf  26136  plyeq0lem  26148  plypf1  26150  plyaddlem  26153  plymullem  26154  plyco  26179  dgreq  26182  0dgrb  26184  coefv0  26186  coeaddlem  26187  coemullem  26188  coemulc  26193  plycn  26199  plycnOLD  26200  dgrcolem2  26213  plycjlem  26215  plycj  26216  plycjOLD  26218  plyrecj  26220  plyreres  26223  dvply1  26224  vieta1lem2  26252  vieta1  26253  elqaalem2  26261  aareccl  26267  aalioulem1  26273  ulmcaulem  26336  ulmcau  26337  ulmcn  26341  mtest  26346  psergf  26354  dvradcnv  26363  psercn2  26365  psercn2OLD  26366  pserdvlem2  26371  pserdv2  26373  abelthlem6  26379  abelthlem8  26382  abelthlem9  26383  logtayl  26602  amgm  26934  ftalem1  27016  ftalem2  27017  ftalem3  27018  ftalem4  27019  ftalem5  27020  basellem2  27025  muinv  27136  dchrmulcl  27193  dchrinvcl  27197  dchrfi  27199  dchrghm  27200  dchrsum2  27212  dchrsum  27213  bposlem5  27232  lgscllem  27248  lgsval4a  27263  lgsneg  27265  lgsdir  27276  lgsdilem2  27277  lgsdi  27278  lgsne0  27279  lgseisenlem3  27321  rpvmasumlem  27431  dchrmusum2  27438  dchrvmasumiflem1  27445  dchrisum0ff  27451  dchrisum0flblem1  27452  dchrisum0fno1  27455  rpvmasum2  27456  dchrisum0re  27457  dchrisum0lem2a  27461  upgrreslem  29284  umgrreslem  29285  wlkpvtx  29638  wlkepvtx  29639  usgr2pthlem  29743  frgrncvvdeqlem8  30285  lnoadd  30737  lnosub  30738  nmosetre  30743  nmooge0  30746  nmoub3i  30752  nmounbi  30755  phoeqi  30836  ubthlem1  30849  h2hcau  30958  h2hlm  30959  hoscl  31724  homcl  31725  hodcl  31726  hoaddcl  31737  homulcl  31738  homullid  31779  homco1  31780  homulass  31781  hoadddi  31782  hoadddir  31783  hoeq1  31809  hoeq2  31810  adjsym  31812  nmopsetretALT  31842  nmfnsetre  31856  cnvadj  31871  hhcno  31883  hhcnf  31884  nmopub2tALT  31888  nmopge0  31890  unopf1o  31895  unoplin  31899  counop  31900  nmfnleub2  31905  nmfnge0  31906  hmoplin  31921  eigvalcl  31940  lnop0  31945  hmops  31999  hmopm  32000  nlelchi  32040  leop2  32103  leopadd  32111  leopmuli  32112  leopnmid  32117  hmopidmchi  32130  pjinvari  32170  sticl  32194  fcomptf  32632  rge0scvg  33932  esumcst  34046  esumfzf  34052  esumfsup  34053  esumfsupre  34054  hasheuni  34068  measdivcstALTV  34208  eulerpartlems  34344  eulerpartlemgc  34346  eulerpartlemb  34352  derangsn  35150  subfacp1lem5  35164  subfacp1lem6  35165  pconnconn  35211  sconnpi1  35219  txsconnlem  35220  cvxsconn  35223  cvmliftphtlem  35297  cvmlift3lem2  35300  cvmlift3lem4  35302  cvmlift3lem6  35304  satfvel  35392  satefvfmla1  35405  elmrsubrn  35500  msubff  35510  msubvrs  35540  mclsssvlem  35542  faclim  35726  curf  37585  uncf  37586  curunc  37589  unccur  37590  matunitlindflem1  37603  matunitlindflem2  37604  ptrecube  37607  heicant  37642  mblfinlem2  37645  itg2addnclem  37658  ftc1anclem1  37680  ftc1anclem2  37681  ftc1anclem4  37683  upixp  37716  fdc  37732  seqpo  37734  incsequz  37735  incsequz2  37736  metf1o  37742  geomcau  37746  sstotbnd2  37761  prdsbnd  37780  ismtyima  37790  ismtyhmeolem  37791  heiborlem3  37800  heiborlem6  37803  heiborlem10  37807  bfplem1  37809  ghomco  37878  sticksstones11  42137  mzpclall  42708  mzprename  42730  rexrabdioph  42775  rmydioph  42996  rmxdioph  42998  expdiophlem2  43004  expdioph  43005  pw2f1ocnv  43019  kelac1  43045  rngunsnply  43151  ofsubid  44306  ofdivrec  44308  ofdivcan4  44309  ofdivdiv2  44310  dvconstbi  44316  refsum2cnlem1  45024  climinf  45597  stoweidlem26  46017  stoweidlem60  46051  stoweid  46054  dmvolsal  46337  caratheodory  46519  elhoi  46533  smfresal  46779  f1oresf1o2  47285  fargshiftf  47434  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  isubgrvtxuhgr  47857  isubgruhgr  47861  isubgr0uhgr  47866  grimuhgr  47880  gricushgr  47910  rmsupp0  48349  domnmsuppn0  48350  gsumlsscl  48361  lincfsuppcl  48395  linccl  48396  lincdifsn  48406  lincsum  48411  lincscm  48412  lincscmcl  48414  lincext1  48436  lindslinindimp2lem1  48440  lindslinindimp2lem4  48443  lindslinindsimp2lem5  48444  snlindsntor  48453  lincresunitlem2  48458  lincresunit3lem1  48461  lincresunit3lem2  48462  lincresunit3  48463  lincreslvec3  48464  isldepslvec2  48467  zlmodzxzldeplem3  48484  1arympt1  48620  ackendofnn0  48666  xpco2  48838  aacllem  49783