Theorem ffvelcdmd 5723

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

Syntax hints:   → wi 4   ∈ wcel 2177  ⟶wf 5272  ‘cfv 5276

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-14 2180  ax-ext 2188  ax-sep 4166  ax-pow 4222  ax-pr 4257

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-sbc 3000  df-un 3171  df-in 3173  df-ss 3180  df-pw 3619  df-sn 3640  df-pr 3641  df-op 3643  df-uni 3853  df-br 4048  df-opab 4110  df-id 4344  df-xp 4685  df-rel 4686  df-cnv 4687  df-co 4688  df-dm 4689  df-rn 4690  df-iota 5237  df-fun 5278  df-fn 5279  df-f 5280  df-fv 5284

This theorem is referenced by:  isotr  5892  caofinvl  6191  rdgon  6479  frecabcl  6492  phplem4dom  6966  fidceq  6973  dif1en  6983  fin0  6989  fin0or  6990  infm  7008  en2eqpr  7011  fidcenumlemrks  7062  fidcenumlemr  7064  supisoti  7119  ordiso2  7144  updjudhcoinlf  7189  updjudhcoinrg  7190  caseinl  7200  caseinr  7201  difinfsnlem  7208  difinfsn  7209  ctmlemr  7217  ctssdclemn0  7219  ctssdc  7222  enumctlemm  7223  enumct  7224  nnnninfeq2  7238  nninfisol  7242  enomnilem  7247  finomni  7249  ismkvnex  7264  enmkvlem  7270  enwomnilem  7278  nninfwlpoimlemg  7284  nninfwlpoimlemginf  7285  exmidfodomrlemr  7317  exmidfodomrlemrALT  7318  acnccim  7391  cauappcvgprlemm  7765  cauappcvgprlemdisj  7771  cauappcvgprlemloc  7772  cauappcvgprlemladdfu  7774  cauappcvgprlemladdru  7776  cauappcvgprlemladdrl  7777  cauappcvgprlem1  7779  cauappcvgprlem2  7780  caucvgprlemnkj  7786  caucvgprlemnbj  7787  caucvgprlemm  7788  caucvgprlemloc  7795  caucvgprlemladdfu  7797  caucvgprlemladdrl  7798  caucvgprlem1  7799  caucvgprlem2  7800  caucvgprprlemnkltj  7809  caucvgprprlemnkeqj  7810  caucvgprprlemnbj  7813  caucvgprprlemmu  7815  caucvgprprlemopl  7817  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  caucvgprprlemexb  7827  caucvgprprlemaddq  7828  caucvgprprlem1  7829  caucvgprprlem2  7830  caucvgsrlemcau  7913  caucvgsrlemgt1  7915  caucvgsrlemoffcau  7918  caucvgsrlemoffres  7920  caucvgsr  7922  axcaucvglemval  8017  axcaucvglemcau  8018  axcaucvglemres  8019  fseq1p1m1  10223  4fvwrd4  10269  fvinim0ffz  10377  frecuzrdgg  10568  frecuzrdgsuctlem  10575  seq3val  10612  seqvalcd  10613  seq3p1  10617  seqp1cd  10622  ser3mono  10639  seq3split  10640  seq3caopr2  10645  iseqf1olemkle  10649  iseqf1olemklt  10650  iseqf1olemqcl  10651  iseqf1olemnab  10653  iseqf1olemmo  10657  iseqf1olemqk  10659  iseqf1olemjpcl  10660  iseqf1olemqpcl  10661  iseqf1olemfvp  10662  seq3f1olemqsumkj  10663  seq3f1olemqsumk  10664  seq3f1olemqsum  10665  seq3f1olemstep  10666  seq3f1oleml  10668  seq3f1o  10669  seqf1oglem2a  10670  seqf1oglem1  10671  seqf1oglem2  10672  seq3z  10680  seq3distr  10684  ser3ge0  10688  ser3le  10689  exp3vallem  10692  exp3val  10693  bcval5  10915  hashfz1  10935  resunimafz0  10983  leisorel  10989  zfz1isolemiso  10991  seq3coll  10994  ccatcl  11057  swrdclg  11111  caucvgrelemcau  11335  caucvgre  11336  cvg1nlemf  11338  cvg1nlemcau  11339  cvg1nlemres  11340  recvguniqlem  11349  resqrexlemdecn  11367  resqrexlemcalc3  11371  resqrexlemnmsq  11372  resqrexlemnm  11373  resqrexlemcvg  11374  resqrexlemoverl  11376  resqrexlemglsq  11377  resqrexlemga  11378  clim2ser  11692  clim2ser2  11693  climrecvg1n  11703  climcvg1nlem  11704  serf0  11707  sumeq2  11714  fsum3cvg  11733  summodclem2a  11736  fsum3  11742  fisumss  11747  fsumcl2lem  11753  fsumadd  11761  fsummulc2  11803  fsumrelem  11826  isumshft  11845  cvgratnnlemseq  11881  cvgratnnlemrate  11885  clim2prod  11894  clim2divap  11895  prodfrecap  11901  prodfdivap  11902  ntrivcvgap  11903  prodeq2  11912  fproddccvg  11927  prodmodclem3  11930  prodmodclem2a  11931  fprodseq  11938  fprodssdc  11945  fprodmul  11946  effsumlt  12047  nninfctlemfo  12405  nn0seqcvgd  12407  ialgrlem1st  12408  eulerthlemrprm  12595  eulerthlema  12596  eulerthlemh  12597  pcmpt2  12711  pcmptdvds  12712  1arithlem4  12733  1arith  12734  ennnfonelemdc  12814  ennnfonelemjn  12817  ennnfonelemg  12818  ennnfonelemp1  12821  ennnfonelemom  12823  ennnfonelemhdmp1  12824  ennnfonelemss  12825  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemex  12829  ennnfonelemhom  12830  ennnfonelemnn0  12837  ennnfonelemim  12839  ctinfomlemom  12842  ctiunctlemudc  12852  ctiunctlemf  12853  ctiunctlemfo  12854  ssnnctlemct  12861  nninfdclemp1  12865  nninfdclemlt  12866  imasmnd2  13328  mhmf1o  13346  mhmco  13366  gsumfzcl  13375  isgrpinv  13430  pwssub  13489  imasgrp2  13490  mhmid  13495  mhmmnd  13496  ghmgrp  13498  mulgval  13502  mulgfng  13504  mulgnnsubcl  13514  ghmid  13629  ghminv  13630  ghmmulg  13636  ghmnsgpreima  13649  ghmeqker  13651  ghmf1  13653  kerf1ghm  13654  ghmf1o  13655  imasring  13870  rhmopp  13982  lspcl  14197  znidomb  14464  znrrg  14466  psrbaglesuppg  14478  psrbagfi  14479  mplsubgfilemcl  14505  iscnp4  14734  cnptopco  14738  lmtopcnp  14766  upxp  14788  uptx  14790  txlm  14795  comet  15015  metcnp3  15027  metcnp  15028  metcnp2  15029  metcnpi3  15033  elcncf2  15090  cncfco  15107  ivthreinc  15161  limcimolemlt  15180  cnplimcim  15183  cnplimclemle  15184  cnplimclemr  15185  limccnpcntop  15191  dvlemap  15196  dvcnp2cntop  15215  dvaddxxbr  15217  dvmulxxbr  15218  dvcoapbr  15223  dvcjbr  15224  dvef  15243  plyaddlem1  15263  plymullem1  15264  plycoeid3  15273  plycolemc  15274  plycjlemc  15276  plycj  15277  plycn  15278  plyrecj  15279  dvply1  15281  dvply2g  15282  lgsval  15525  lgscllem  15528  lgsval2lem  15531  lgsval4a  15543  lgsneg  15545  lgsdir  15556  lgsdilem2  15557  lgsdi  15558  lgsne0  15559  lgseisenlem3  15593  lgseisenlem4  15594  1dom1el  16001  2omap  16006  pwle2  16009  subctctexmid  16011  nnsf  16016  peano4nninf  16017  nninfalllem1  16019  nninfsellemdc  16021  nninfsellemeq  16025  nninfsellemqall  16026  nninfsellemeqinf  16027  nninfomnilem  16029  nnnninfex  16033  nninfnfiinf  16034  isomninnlem  16043  trilpolemeq1  16053  trilpolemlt1  16054  iswomninnlem  16062  iswomni0  16064  ismkvnnlem  16065  nconstwlpolemgt0  16077  nconstwlpolem  16078