Theorem ffvelrnd 5508

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

Syntax hints:   → wi 4   ∈ wcel 1461  ⟶wf 5075  ‘cfv 5079

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-10 1464  ax-11 1465  ax-i12 1466  ax-bndl 1467  ax-4 1468  ax-14 1473  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095  ax-sep 4004  ax-pow 4056  ax-pr 4089

This theorem depends on definitions:  df-bi 116  df-3an 945  df-tru 1315  df-nf 1418  df-sb 1717  df-eu 1976  df-mo 1977  df-clab 2100  df-cleq 2106  df-clel 2109  df-nfc 2242  df-ral 2393  df-rex 2394  df-v 2657  df-sbc 2877  df-un 3039  df-in 3041  df-ss 3048  df-pw 3476  df-sn 3497  df-pr 3498  df-op 3500  df-uni 3701  df-br 3894  df-opab 3948  df-id 4173  df-xp 4503  df-rel 4504  df-cnv 4505  df-co 4506  df-dm 4507  df-rn 4508  df-iota 5044  df-fun 5081  df-fn 5082  df-f 5083  df-fv 5087

This theorem is referenced by:  isotr  5669  caofinvl  5956  rdgon  6235  frecabcl  6248  phplem4dom  6707  fidceq  6714  dif1en  6724  fin0  6730  fin0or  6731  infm  6749  en2eqpr  6752  fidcenumlemrks  6791  fidcenumlemr  6793  supisoti  6847  ordiso2  6870  updjudhcoinlf  6915  updjudhcoinrg  6916  caseinl  6926  caseinr  6927  difinfsnlem  6934  difinfsn  6935  ctmlemr  6943  ctssdclemn0  6945  ctssdc  6948  enumctlemm  6949  enumct  6950  enomnilem  6958  finomni  6960  exmidfodomrlemr  7003  exmidfodomrlemrALT  7004  cauappcvgprlemm  7395  cauappcvgprlemdisj  7401  cauappcvgprlemloc  7402  cauappcvgprlemladdfu  7404  cauappcvgprlemladdru  7406  cauappcvgprlemladdrl  7407  cauappcvgprlem1  7409  cauappcvgprlem2  7410  caucvgprlemnkj  7416  caucvgprlemnbj  7417  caucvgprlemm  7418  caucvgprlemloc  7425  caucvgprlemladdfu  7427  caucvgprlemladdrl  7428  caucvgprlem1  7429  caucvgprlem2  7430  caucvgprprlemnkltj  7439  caucvgprprlemnkeqj  7440  caucvgprprlemnbj  7443  caucvgprprlemmu  7445  caucvgprprlemopl  7447  caucvgprprlemloc  7453  caucvgprprlemexbt  7456  caucvgprprlemexb  7457  caucvgprprlemaddq  7458  caucvgprprlem1  7459  caucvgprprlem2  7460  caucvgsrlemcau  7529  caucvgsrlemgt1  7531  caucvgsrlemoffcau  7534  caucvgsrlemoffres  7536  caucvgsr  7538  axcaucvglemval  7626  axcaucvglemcau  7627  axcaucvglemres  7628  fseq1p1m1  9761  4fvwrd4  9804  fvinim0ffz  9905  frecuzrdgg  10076  frecuzrdgsuctlem  10083  seq3val  10118  seqvalcd  10119  seq3p1  10122  seqp1cd  10126  ser3mono  10138  seq3split  10139  seq3caopr2  10142  iseqf1olemkle  10144  iseqf1olemklt  10145  iseqf1olemqcl  10146  iseqf1olemnab  10148  iseqf1olemmo  10152  iseqf1olemqk  10154  iseqf1olemjpcl  10155  iseqf1olemqpcl  10156  iseqf1olemfvp  10157  seq3f1olemqsumkj  10158  seq3f1olemqsumk  10159  seq3f1olemqsum  10160  seq3f1olemstep  10161  seq3f1oleml  10163  seq3f1o  10164  seq3z  10171  seq3distr  10173  ser3ge0  10177  ser3le  10178  exp3vallem  10181  exp3val  10182  bcval5  10396  hashfz1  10416  resunimafz0  10461  leisorel  10467  zfz1isolemiso  10469  seq3coll  10472  caucvgrelemcau  10638  caucvgre  10639  cvg1nlemf  10641  cvg1nlemcau  10642  cvg1nlemres  10643  recvguniqlem  10652  resqrexlemdecn  10670  resqrexlemcalc3  10674  resqrexlemnmsq  10675  resqrexlemnm  10676  resqrexlemcvg  10677  resqrexlemoverl  10679  resqrexlemglsq  10680  resqrexlemga  10681  clim2ser  10992  clim2ser2  10993  climrecvg1n  11003  climcvg1nlem  11004  serf0  11007  sumeq2  11014  fsum3cvg  11032  summodclem2a  11036  fsum3  11042  fisumss  11047  fsumcl2lem  11053  fsumadd  11061  fsummulc2  11103  fsumrelem  11126  isumshft  11145  cvgratnnlemseq  11181  cvgratnnlemrate  11185  effsumlt  11243  nn0seqcvgd  11562  ialgrlem1st  11563  ennnfonelemdc  11751  ennnfonelemjn  11754  ennnfonelemg  11755  ennnfonelemp1  11758  ennnfonelemom  11760  ennnfonelemhdmp1  11761  ennnfonelemss  11762  ennnfonelemkh  11764  ennnfonelemhf1o  11765  ennnfonelemex  11766  ennnfonelemhom  11767  ennnfonelemnn0  11774  ennnfonelemim  11776  ctinfomlemom  11779  ctiunctlemudc  11787  ctiunctlemf  11788  ctiunctlemfo  11789  iscnp4  12223  cnptopco  12227  lmtopcnp  12255  upxp  12277  uptx  12279  txlm  12284  comet  12482  metcnp3  12494  metcnp  12495  metcnp2  12496  metcnpi3  12500  elcncf2  12541  cncfco  12558  limcimolemlt  12583  cnplimcim  12586  cnplimclemle  12587  cnplimclemr  12588  limccnpcntop  12594  dvlemap  12598  dvcnp2cntop  12612  dvaddxxbr  12614  pwle2  12876  nnsf  12880  peano4nninf  12881  nninfalllem1  12884  nninfsellemdc  12887  nninfsellemeq  12891  nninfsellemqall  12892  nninfsellemeqinf  12893  nninfomnilem  12895  isomninnlem  12906  trilpolemeq1  12914  trilpolemlt1  12915