Theorem ffvelcdmd 5844

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypotheses

Ref	Expression
ffvelcdmd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
ffvelcdmd.2	⊢ (𝜑 → 𝐶 ∈ 𝐴)

Assertion

Ref	Expression
ffvelcdmd	⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

Proof of Theorem ffvelcdmd

Step	Hyp	Ref	Expression
1		ffvelcdmd.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		ffvelcdmd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3	2	ffvelcdmda 5843	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
4	1, 3	mpdan 425	1 ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ⟶wf 5373  ‘cfv 5377

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4249  ax-pow 4311  ax-pr 4346

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-opab 4193  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-fv 5385

This theorem is used by:  isotr  6022  caofinvl  6328  fvdifsuppst  6484  rdgon  6657  frecabcl  6670  1dom1el  7107  phplem4dom  7163  fidceq  7171  dif1en  7183  fin0  7189  fin0or  7190  infm  7211  en2eqpr  7214  fidcenumlemrks  7270  fidcenumlemr  7272  fdcf1  7316  2omap  7318  supisoti  7350  ordiso2  7375  updjudhcoinlf  7420  updjudhcoinrg  7421  caseinl  7431  caseinr  7432  difinfsnlem  7439  difinfsn  7440  ctmlemr  7448  ctssdclemn0  7450  ctssdc  7453  enumctlemm  7454  enumct  7455  nnnninfeq2  7469  nninfisol  7473  enomnilem  7478  finomni  7480  ismkvnex  7495  enmkvlem  7501  enwomnilem  7509  nninfwlpoimlemg  7515  nninfwlpoimlemginf  7516  pr2cv1  7541  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  acnccim  7638  cauappcvgprlemm  8012  cauappcvgprlemdisj  8018  cauappcvgprlemloc  8019  cauappcvgprlemladdfu  8021  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlem2  8027  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemloc  8042  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgprlem2  8047  caucvgprprlemnkltj  8056  caucvgprprlemnkeqj  8057  caucvgprprlemnbj  8060  caucvgprprlemmu  8062  caucvgprprlemopl  8064  caucvgprprlemloc  8070  caucvgprprlemexbt  8073  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  caucvgprprlem2  8077  caucvgsrlemcau  8160  caucvgsrlemgt1  8162  caucvgsrlemoffcau  8165  caucvgsrlemoffres  8167  caucvgsr  8169  axcaucvglemval  8264  axcaucvglemcau  8265  axcaucvglemres  8266  fseq1p1m1  10503  4fvwrd4  10549  fvinim0ffz  10662  frecuzrdgg  10855  frecuzrdgsuctlem  10862  seq3val  10899  seqvalcd  10900  seq3p1  10904  seqp1cd  10909  ser3mono  10926  seq3split  10927  seq3caopr2  10932  iseqf1olemkle  10936  iseqf1olemklt  10937  iseqf1olemqcl  10938  iseqf1olemnab  10940  iseqf1olemmo  10944  iseqf1olemqk  10946  iseqf1olemjpcl  10947  iseqf1olemqpcl  10948  iseqf1olemfvp  10949  seq3f1olemqsumkj  10950  seq3f1olemqsumk  10951  seq3f1olemqsum  10952  seq3f1olemstep  10953  seq3f1oleml  10955  seq3f1o  10956  seqf1oglem2a  10957  seqf1oglem1  10958  seqf1oglem2  10959  seq3z  10967  seq3distr  10971  ser3ge0  10975  ser3le  10976  exp3vallem  10979  exp3val  10980  bcval5  11203  hashfz1  11224  resunimafz0  11276  leisorel  11291  zfz1isolemiso  11293  seq3coll  11296  ccatcl  11363  swrdclg  11424  caucvgrelemcau  11748  caucvgre  11749  cvg1nlemf  11751  cvg1nlemcau  11752  cvg1nlemres  11753  recvguniqlem  11762  resqrexlemdecn  11780  resqrexlemcalc3  11784  resqrexlemnmsq  11785  resqrexlemnm  11786  resqrexlemcvg  11787  resqrexlemoverl  11789  resqrexlemglsq  11790  resqrexlemga  11791  clim2ser  12105  clim2ser2  12106  climrecvg1n  12116  climcvg1nlem  12117  serf0  12120  sumeq2  12127  fsum3cvg  12147  summodclem2a  12150  fsum3  12156  fisumss  12161  fsumcl2lem  12167  fsumadd  12175  fsummulc2  12217  fsumrelem  12240  isumshft  12259  cvgratnnlemseq  12295  cvgratnnlemrate  12299  clim2prod  12308  clim2divap  12309  prodfrecap  12315  prodfdivap  12316  ntrivcvgap  12317  prodeq2  12326  fproddccvg  12341  prodmodclem3  12344  prodmodclem2a  12345  fprodseq  12352  fprodssdc  12359  fprodmul  12360  effsumlt  12461  nninfctlemfo  12819  nn0seqcvgd  12821  ialgrlem1st  12822  eulerthlemrprm  13009  eulerthlema  13010  eulerthlemh  13011  pcmpt2  13125  pcmptdvds  13126  1arithlem4  13147  1arith  13148  ennnfonelemdc  13292  ennnfonelemjn  13295  ennnfonelemg  13296  ennnfonelemp1  13299  ennnfonelemom  13301  ennnfonelemhdmp1  13302  ennnfonelemss  13303  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemex  13307  ennnfonelemhom  13308  ennnfonelemnn0  13315  ennnfonelemim  13317  ctinfomlemom  13320  ctiunctlemudc  13330  ctiunctlemf  13331  ctiunctlemfo  13332  ssnnctlemct  13339  nninfdclemp1  13343  nninfdclemlt  13344  imasmnd2  13761  mhmf1o  13779  mhmco  13799  gzsumcl  13806  isgrpinv  13861  imasgrp2  13915  mhmid  13920  mhmmnd  13921  ghmgrp  13923  mulgval  13927  mulgfng  13929  mulgnnsubcl  13939  ghmid  14054  ghminv  14055  ghmmulg  14061  ghmnsgpreima  14074  ghmeqker  14076  ghmf1  14078  kerf1ghm  14079  ghmf1o  14080  gzsumsplit0  14150  gsumvalfi  14154  gsumclfi  14161  gsumsubmclfi  14165  pwssub  14218  imasring  14371  rhmopp  14485  lspcl  14730  znidomb  14995  znrrg  14997  asclelbas  15028  psrbaglesuppg  15059  psrbagfi  15061  psrbaglecl  15062  psrbagcon  15064  mplsubgfilemcl  15092  iscnp4  15321  cnptopco  15325  lmtopcnp  15353  upxp  15375  uptx  15377  txlm  15382  comet  15602  metcnp3  15614  metcnp  15615  metcnp2  15616  metcnpi3  15620  elcncf2  15677  cncfco  15694  ivthreinc  15748  limcimolemlt  15767  cnplimcim  15770  cnplimclemle  15771  cnplimclemr  15772  limccnpcntop  15778  dvlemap  15783  dvcnp2cntop  15802  dvaddxxbr  15804  dvmulxxbr  15805  dvcoapbr  15810  dvcjbr  15811  dvef  15830  plyaddlem1  15850  plymullem1  15851  plycoeid3  15860  plycolemc  15861  plycjlemc  15863  plycj  15864  plycn  15865  plyrecj  15866  dvply1  15868  dvply2g  15869  logfac  16001  lgsval  16135  lgscllem  16138  lgsval2lem  16141  lgsval4a  16153  lgsneg  16155  lgsdir  16166  lgsdilem2  16167  lgsdi  16168  lgsne0  16169  lgseisenlem3  16203  lgseisenlem4  16204  p1evtxdeqfi  16565  wlkvtxm  16593  wlkvtxiedg  16598  wlkvtxiedgg  16599  upgriswlkdc  16613  trlsegvdeglem7  16719  trlsegvdegfi  16720  eupth2lem3lem1fi  16721  eupth2lem3lem2fi  16722  eupth2lem3lem3fi  16723  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  eupth2lem3lem7fi  16727  eupth2lemsfi  16731  3dom  17030  pwle2  17040  subctctexmid  17042  nnsf  17060  peano4nninf  17061  nninfalllem1  17063  nninfsellemdc  17065  nninfsellemeq  17069  nninfsellemqall  17070  nninfsellemeqinf  17071  nninfomnilem  17073  nnnninfex  17077  nninfnfiinf  17078  repiecelem  17086  repiecele0  17087  repiecege0  17088  isomninnlem  17091  trilpolemeq1  17101  trilpolemlt1  17102  iswomninnlem  17111  iswomni0  17113  ismkvnnlem  17114  nconstwlpolemgt0  17126  nconstwlpolem  17127