Theorem ffvelcdmd 5695

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

Syntax hints:   → wi 4   ∈ wcel 2164  ⟶wf 5251  ‘cfv 5255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ral 2477  df-rex 2478  df-v 2762  df-sbc 2987  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-rn 4671  df-iota 5216  df-fun 5257  df-fn 5258  df-f 5259  df-fv 5263

This theorem is referenced by:  isotr  5860  caofinvl  6157  rdgon  6441  frecabcl  6454  phplem4dom  6920  fidceq  6927  dif1en  6937  fin0  6943  fin0or  6944  infm  6962  en2eqpr  6965  fidcenumlemrks  7014  fidcenumlemr  7016  supisoti  7071  ordiso2  7096  updjudhcoinlf  7141  updjudhcoinrg  7142  caseinl  7152  caseinr  7153  difinfsnlem  7160  difinfsn  7161  ctmlemr  7169  ctssdclemn0  7171  ctssdc  7174  enumctlemm  7175  enumct  7176  nnnninfeq2  7190  nninfisol  7194  enomnilem  7199  finomni  7201  ismkvnex  7216  enmkvlem  7222  enwomnilem  7230  nninfwlpoimlemg  7236  nninfwlpoimlemginf  7237  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  cauappcvgprlemm  7707  cauappcvgprlemdisj  7713  cauappcvgprlemloc  7714  cauappcvgprlemladdfu  7716  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  cauappcvgprlem1  7721  cauappcvgprlem2  7722  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprlem1  7741  caucvgprlem2  7742  caucvgprprlemnkltj  7751  caucvgprprlemnkeqj  7752  caucvgprprlemnbj  7755  caucvgprprlemmu  7757  caucvgprprlemopl  7759  caucvgprprlemloc  7765  caucvgprprlemexbt  7768  caucvgprprlemexb  7769  caucvgprprlemaddq  7770  caucvgprprlem1  7771  caucvgprprlem2  7772  caucvgsrlemcau  7855  caucvgsrlemgt1  7857  caucvgsrlemoffcau  7860  caucvgsrlemoffres  7862  caucvgsr  7864  axcaucvglemval  7959  axcaucvglemcau  7960  axcaucvglemres  7961  fseq1p1m1  10163  4fvwrd4  10209  fvinim0ffz  10311  frecuzrdgg  10490  frecuzrdgsuctlem  10497  seq3val  10534  seqvalcd  10535  seq3p1  10539  seqp1cd  10544  ser3mono  10561  seq3split  10562  seq3caopr2  10567  iseqf1olemkle  10571  iseqf1olemklt  10572  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemmo  10579  iseqf1olemqk  10581  iseqf1olemjpcl  10582  iseqf1olemqpcl  10583  iseqf1olemfvp  10584  seq3f1olemqsumkj  10585  seq3f1olemqsumk  10586  seq3f1olemqsum  10587  seq3f1olemstep  10588  seq3f1oleml  10590  seq3f1o  10591  seqf1oglem2a  10592  seqf1oglem1  10593  seqf1oglem2  10594  seq3z  10602  seq3distr  10606  ser3ge0  10610  ser3le  10611  exp3vallem  10614  exp3val  10615  bcval5  10837  hashfz1  10857  resunimafz0  10905  leisorel  10911  zfz1isolemiso  10913  seq3coll  10916  caucvgrelemcau  11127  caucvgre  11128  cvg1nlemf  11130  cvg1nlemcau  11131  cvg1nlemres  11132  recvguniqlem  11141  resqrexlemdecn  11159  resqrexlemcalc3  11163  resqrexlemnmsq  11164  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemoverl  11168  resqrexlemglsq  11169  resqrexlemga  11170  clim2ser  11483  clim2ser2  11484  climrecvg1n  11494  climcvg1nlem  11495  serf0  11498  sumeq2  11505  fsum3cvg  11524  summodclem2a  11527  fsum3  11533  fisumss  11538  fsumcl2lem  11544  fsumadd  11552  fsummulc2  11594  fsumrelem  11617  isumshft  11636  cvgratnnlemseq  11672  cvgratnnlemrate  11676  clim2prod  11685  clim2divap  11686  prodfrecap  11692  prodfdivap  11693  ntrivcvgap  11694  prodeq2  11703  fproddccvg  11718  prodmodclem3  11721  prodmodclem2a  11722  fprodseq  11729  fprodssdc  11736  fprodmul  11737  effsumlt  11838  nninfctlemfo  12180  nn0seqcvgd  12182  ialgrlem1st  12183  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  pcmpt2  12485  pcmptdvds  12486  1arithlem4  12507  1arith  12508  ennnfonelemdc  12559  ennnfonelemjn  12562  ennnfonelemg  12563  ennnfonelemp1  12566  ennnfonelemom  12568  ennnfonelemhdmp1  12569  ennnfonelemss  12570  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemhom  12575  ennnfonelemnn0  12582  ennnfonelemim  12584  ctinfomlemom  12587  ctiunctlemudc  12597  ctiunctlemf  12598  ctiunctlemfo  12599  ssnnctlemct  12606  nninfdclemp1  12610  nninfdclemlt  12611  mhmf1o  13045  mhmco  13065  gsumfzcl  13074  isgrpinv  13129  imasgrp2  13183  mhmid  13188  mhmmnd  13189  ghmgrp  13191  mulgval  13195  mulgfng  13197  mulgnnsubcl  13207  ghmid  13322  ghminv  13323  ghmmulg  13329  ghmnsgpreima  13342  ghmeqker  13344  ghmf1  13346  kerf1ghm  13347  ghmf1o  13348  imasring  13563  rhmopp  13675  lspcl  13890  znidomb  14157  znrrg  14159  psrbaglesuppg  14169  iscnp4  14397  cnptopco  14401  lmtopcnp  14429  upxp  14451  uptx  14453  txlm  14458  comet  14678  metcnp3  14690  metcnp  14691  metcnp2  14692  metcnpi3  14696  elcncf2  14753  cncfco  14770  ivthreinc  14824  limcimolemlt  14843  cnplimcim  14846  cnplimclemle  14847  cnplimclemr  14848  limccnpcntop  14854  dvlemap  14859  dvcnp2cntop  14878  dvaddxxbr  14880  dvmulxxbr  14881  dvcoapbr  14886  dvcjbr  14887  dvef  14906  plyaddlem1  14926  plymullem1  14927  plycolemc  14936  plycjlemc  14938  plycj  14939  plycn  14940  plyrecj  14941  dvply1  14943  lgsval  15161  lgscllem  15164  lgsval2lem  15167  lgsval4a  15179  lgsneg  15181  lgsdir  15192  lgsdilem2  15193  lgsdi  15194  lgsne0  15195  lgseisenlem3  15229  lgseisenlem4  15230  1dom1el  15553  pwle2  15559  subctctexmid  15561  nnsf  15565  peano4nninf  15566  nninfalllem1  15568  nninfsellemdc  15570  nninfsellemeq  15574  nninfsellemqall  15575  nninfsellemeqinf  15576  nninfomnilem  15578  isomninnlem  15590  trilpolemeq1  15600  trilpolemlt1  15601  iswomninnlem  15609  iswomni0  15611  ismkvnnlem  15612  nconstwlpolemgt0  15624  nconstwlpolem  15625