Theorem ffvelrnd 5621

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 5620	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ 𝐴) → (𝐹‘𝐶) ∈ 𝐵)
4	1, 3	mpdan 418	1 ⊢ (𝜑 → (𝐹‘𝐶) ∈ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2136  ⟶wf 5184  ‘cfv 5188

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-14 2139  ax-ext 2147  ax-sep 4100  ax-pow 4153  ax-pr 4187

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-eu 2017  df-mo 2018  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-ral 2449  df-rex 2450  df-v 2728  df-sbc 2952  df-un 3120  df-in 3122  df-ss 3129  df-pw 3561  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-opab 4044  df-id 4271  df-xp 4610  df-rel 4611  df-cnv 4612  df-co 4613  df-dm 4614  df-rn 4615  df-iota 5153  df-fun 5190  df-fn 5191  df-f 5192  df-fv 5196

This theorem is referenced by:  isotr  5784  caofinvl  6072  rdgon  6354  frecabcl  6367  phplem4dom  6828  fidceq  6835  dif1en  6845  fin0  6851  fin0or  6852  infm  6870  en2eqpr  6873  fidcenumlemrks  6918  fidcenumlemr  6920  supisoti  6975  ordiso2  7000  updjudhcoinlf  7045  updjudhcoinrg  7046  caseinl  7056  caseinr  7057  difinfsnlem  7064  difinfsn  7065  ctmlemr  7073  ctssdclemn0  7075  ctssdc  7078  enumctlemm  7079  enumct  7080  nnnninfeq2  7093  nninfisol  7097  enomnilem  7102  finomni  7104  ismkvnex  7119  enmkvlem  7125  enwomnilem  7133  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  cauappcvgprlemm  7586  cauappcvgprlemdisj  7592  cauappcvgprlemloc  7593  cauappcvgprlemladdfu  7595  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlem2  7601  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemloc  7616  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprlem1  7620  caucvgprlem2  7621  caucvgprprlemnkltj  7630  caucvgprprlemnkeqj  7631  caucvgprprlemnbj  7634  caucvgprprlemmu  7636  caucvgprprlemopl  7638  caucvgprprlemloc  7644  caucvgprprlemexbt  7647  caucvgprprlemexb  7648  caucvgprprlemaddq  7649  caucvgprprlem1  7650  caucvgprprlem2  7651  caucvgsrlemcau  7734  caucvgsrlemgt1  7736  caucvgsrlemoffcau  7739  caucvgsrlemoffres  7741  caucvgsr  7743  axcaucvglemval  7838  axcaucvglemcau  7839  axcaucvglemres  7840  fseq1p1m1  10029  4fvwrd4  10075  fvinim0ffz  10176  frecuzrdgg  10351  frecuzrdgsuctlem  10358  seq3val  10393  seqvalcd  10394  seq3p1  10397  seqp1cd  10401  ser3mono  10413  seq3split  10414  seq3caopr2  10417  iseqf1olemkle  10419  iseqf1olemklt  10420  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemmo  10427  iseqf1olemqk  10429  iseqf1olemjpcl  10430  iseqf1olemqpcl  10431  iseqf1olemfvp  10432  seq3f1olemqsumkj  10433  seq3f1olemqsumk  10434  seq3f1olemqsum  10435  seq3f1olemstep  10436  seq3f1oleml  10438  seq3f1o  10439  seq3z  10446  seq3distr  10448  ser3ge0  10452  ser3le  10453  exp3vallem  10456  exp3val  10457  bcval5  10676  hashfz1  10696  resunimafz0  10744  leisorel  10750  zfz1isolemiso  10752  seq3coll  10755  caucvgrelemcau  10922  caucvgre  10923  cvg1nlemf  10925  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniqlem  10936  resqrexlemdecn  10954  resqrexlemcalc3  10958  resqrexlemnmsq  10959  resqrexlemnm  10960  resqrexlemcvg  10961  resqrexlemoverl  10963  resqrexlemglsq  10964  resqrexlemga  10965  clim2ser  11278  clim2ser2  11279  climrecvg1n  11289  climcvg1nlem  11290  serf0  11293  sumeq2  11300  fsum3cvg  11319  summodclem2a  11322  fsum3  11328  fisumss  11333  fsumcl2lem  11339  fsumadd  11347  fsummulc2  11389  fsumrelem  11412  isumshft  11431  cvgratnnlemseq  11467  cvgratnnlemrate  11471  clim2prod  11480  clim2divap  11481  prodfrecap  11487  prodfdivap  11488  ntrivcvgap  11489  prodeq2  11498  fproddccvg  11513  prodmodclem3  11516  prodmodclem2a  11517  fprodseq  11524  fprodssdc  11531  fprodmul  11532  effsumlt  11633  nn0seqcvgd  11973  ialgrlem1st  11974  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  pcmpt2  12274  pcmptdvds  12275  1arithlem4  12296  1arith  12297  ennnfonelemdc  12332  ennnfonelemjn  12335  ennnfonelemg  12336  ennnfonelemp1  12339  ennnfonelemom  12341  ennnfonelemhdmp1  12342  ennnfonelemss  12343  ennnfonelemkh  12345  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemhom  12348  ennnfonelemnn0  12355  ennnfonelemim  12357  ctinfomlemom  12360  ctiunctlemudc  12370  ctiunctlemf  12371  ctiunctlemfo  12372  ssnnctlemct  12379  nninfdclemp1  12383  nninfdclemlt  12384  iscnp4  12858  cnptopco  12862  lmtopcnp  12890  upxp  12912  uptx  12914  txlm  12919  comet  13139  metcnp3  13151  metcnp  13152  metcnp2  13153  metcnpi3  13157  elcncf2  13201  cncfco  13218  limcimolemlt  13273  cnplimcim  13276  cnplimclemle  13277  cnplimclemr  13278  limccnpcntop  13284  dvlemap  13289  dvcnp2cntop  13303  dvaddxxbr  13305  dvmulxxbr  13306  dvcoapbr  13311  dvcjbr  13312  dvef  13328  lgsval  13545  lgscllem  13548  lgsval2lem  13551  lgsval4a  13563  lgsneg  13565  lgsdir  13576  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  pwle2  13878  subctctexmid  13881  nnsf  13885  peano4nninf  13886  nninfalllem1  13888  nninfsellemdc  13890  nninfsellemeq  13894  nninfsellemqall  13895  nninfsellemeqinf  13896  nninfomnilem  13898  isomninnlem  13909  trilpolemeq1  13919  trilpolemlt1  13920  iswomninnlem  13928  iswomni0  13930  ismkvnnlem  13931  nconstwlpolemgt0  13942  nconstwlpolem  13943