Theorem ffvelrnd 5615

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

Hypotheses

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

Assertion

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

Proof of Theorem ffvelrnd

Step	Hyp	Ref	Expression
1		ffvelrnd.2	. 2 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
2		ffvelrnd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
3	2	ffvelrnda 5614	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
4	1, 3	mpdan 418	1 ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2135  ⟶wf 5178  ‘cfv 5182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447  df-rex 2448  df-v 2723  df-sbc 2947  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-rn 4609  df-iota 5147  df-fun 5184  df-fn 5185  df-f 5186  df-fv 5190

This theorem is referenced by:  isotr  5778  caofinvl  6066  rdgon  6345  frecabcl  6358  phplem4dom  6819  fidceq  6826  dif1en  6836  fin0  6842  fin0or  6843  infm  6861  en2eqpr  6864  fidcenumlemrks  6909  fidcenumlemr  6911  supisoti  6966  ordiso2  6991  updjudhcoinlf  7036  updjudhcoinrg  7037  caseinl  7047  caseinr  7048  difinfsnlem  7055  difinfsn  7056  ctmlemr  7064  ctssdclemn0  7066  ctssdc  7069  enumctlemm  7070  enumct  7071  nnnninfeq2  7084  nninfisol  7088  enomnilem  7093  finomni  7095  ismkvnex  7110  enmkvlem  7116  enwomnilem  7124  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  cauappcvgprlemm  7577  cauappcvgprlemdisj  7583  cauappcvgprlemloc  7584  cauappcvgprlemladdfu  7586  cauappcvgprlemladdru  7588  cauappcvgprlemladdrl  7589  cauappcvgprlem1  7591  cauappcvgprlem2  7592  caucvgprlemnkj  7598  caucvgprlemnbj  7599  caucvgprlemm  7600  caucvgprlemloc  7607  caucvgprlemladdfu  7609  caucvgprlemladdrl  7610  caucvgprlem1  7611  caucvgprlem2  7612  caucvgprprlemnkltj  7621  caucvgprprlemnkeqj  7622  caucvgprprlemnbj  7625  caucvgprprlemmu  7627  caucvgprprlemopl  7629  caucvgprprlemloc  7635  caucvgprprlemexbt  7638  caucvgprprlemexb  7639  caucvgprprlemaddq  7640  caucvgprprlem1  7641  caucvgprprlem2  7642  caucvgsrlemcau  7725  caucvgsrlemgt1  7727  caucvgsrlemoffcau  7730  caucvgsrlemoffres  7732  caucvgsr  7734  axcaucvglemval  7829  axcaucvglemcau  7830  axcaucvglemres  7831  fseq1p1m1  10019  4fvwrd4  10065  fvinim0ffz  10166  frecuzrdgg  10341  frecuzrdgsuctlem  10348  seq3val  10383  seqvalcd  10384  seq3p1  10387  seqp1cd  10391  ser3mono  10403  seq3split  10404  seq3caopr2  10407  iseqf1olemkle  10409  iseqf1olemklt  10410  iseqf1olemqcl  10411  iseqf1olemnab  10413  iseqf1olemmo  10417  iseqf1olemqk  10419  iseqf1olemjpcl  10420  iseqf1olemqpcl  10421  iseqf1olemfvp  10422  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3f1olemqsum  10425  seq3f1olemstep  10426  seq3f1oleml  10428  seq3f1o  10429  seq3z  10436  seq3distr  10438  ser3ge0  10442  ser3le  10443  exp3vallem  10446  exp3val  10447  bcval5  10665  hashfz1  10685  resunimafz0  10730  leisorel  10736  zfz1isolemiso  10738  seq3coll  10741  caucvgrelemcau  10908  caucvgre  10909  cvg1nlemf  10911  cvg1nlemcau  10912  cvg1nlemres  10913  recvguniqlem  10922  resqrexlemdecn  10940  resqrexlemcalc3  10944  resqrexlemnmsq  10945  resqrexlemnm  10946  resqrexlemcvg  10947  resqrexlemoverl  10949  resqrexlemglsq  10950  resqrexlemga  10951  clim2ser  11264  clim2ser2  11265  climrecvg1n  11275  climcvg1nlem  11276  serf0  11279  sumeq2  11286  fsum3cvg  11305  summodclem2a  11308  fsum3  11314  fisumss  11319  fsumcl2lem  11325  fsumadd  11333  fsummulc2  11375  fsumrelem  11398  isumshft  11417  cvgratnnlemseq  11453  cvgratnnlemrate  11457  clim2prod  11466  clim2divap  11467  prodfrecap  11473  prodfdivap  11474  ntrivcvgap  11475  prodeq2  11484  fproddccvg  11499  prodmodclem3  11502  prodmodclem2a  11503  fprodseq  11510  fprodssdc  11517  fprodmul  11518  effsumlt  11619  nn0seqcvgd  11952  ialgrlem1st  11953  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  pcmpt2  12251  pcmptdvds  12252  ennnfonelemdc  12269  ennnfonelemjn  12272  ennnfonelemg  12273  ennnfonelemp1  12276  ennnfonelemom  12278  ennnfonelemhdmp1  12279  ennnfonelemss  12280  ennnfonelemkh  12282  ennnfonelemhf1o  12283  ennnfonelemex  12284  ennnfonelemhom  12285  ennnfonelemnn0  12292  ennnfonelemim  12294  ctinfomlemom  12297  ctiunctlemudc  12307  ctiunctlemf  12308  ctiunctlemfo  12309  ssnnctlemct  12316  nninfdclemp1  12322  nninfdclemlt  12323  iscnp4  12759  cnptopco  12763  lmtopcnp  12791  upxp  12813  uptx  12815  txlm  12820  comet  13040  metcnp3  13052  metcnp  13053  metcnp2  13054  metcnpi3  13058  elcncf2  13102  cncfco  13119  limcimolemlt  13174  cnplimcim  13177  cnplimclemle  13178  cnplimclemr  13179  limccnpcntop  13185  dvlemap  13190  dvcnp2cntop  13204  dvaddxxbr  13206  dvmulxxbr  13207  dvcoapbr  13212  dvcjbr  13213  dvef  13229  pwle2  13712  subctctexmid  13715  nnsf  13719  peano4nninf  13720  nninfalllem1  13722  nninfsellemdc  13724  nninfsellemeq  13728  nninfsellemqall  13729  nninfsellemeqinf  13730  nninfomnilem  13732  isomninnlem  13743  trilpolemeq1  13753  trilpolemlt1  13754  iswomninnlem  13762  iswomni0  13764  ismkvnnlem  13765  nconstwlpolemgt0  13776  nconstwlpolem  13777