Theorem ffvelcdmd 5701

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

Syntax hints:   → wi 4   ∈ wcel 2167  ⟶wf 5255  ‘cfv 5259

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-rex 2481  df-v 2765  df-sbc 2990  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-opab 4096  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-rn 4675  df-iota 5220  df-fun 5261  df-fn 5262  df-f 5263  df-fv 5267

This theorem is referenced by:  isotr  5866  caofinvl  6165  rdgon  6453  frecabcl  6466  phplem4dom  6932  fidceq  6939  dif1en  6949  fin0  6955  fin0or  6956  infm  6974  en2eqpr  6977  fidcenumlemrks  7028  fidcenumlemr  7030  supisoti  7085  ordiso2  7110  updjudhcoinlf  7155  updjudhcoinrg  7156  caseinl  7166  caseinr  7167  difinfsnlem  7174  difinfsn  7175  ctmlemr  7183  ctssdclemn0  7185  ctssdc  7188  enumctlemm  7189  enumct  7190  nnnninfeq2  7204  nninfisol  7208  enomnilem  7213  finomni  7215  ismkvnex  7230  enmkvlem  7236  enwomnilem  7244  nninfwlpoimlemg  7250  nninfwlpoimlemginf  7251  exmidfodomrlemr  7281  exmidfodomrlemrALT  7282  acnccim  7355  cauappcvgprlemm  7729  cauappcvgprlemdisj  7735  cauappcvgprlemloc  7736  cauappcvgprlemladdfu  7738  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  cauappcvgprlem1  7743  cauappcvgprlem2  7744  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemloc  7759  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprlem1  7763  caucvgprlem2  7764  caucvgprprlemnkltj  7773  caucvgprprlemnkeqj  7774  caucvgprprlemnbj  7777  caucvgprprlemmu  7779  caucvgprprlemopl  7781  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  caucvgprprlemexb  7791  caucvgprprlemaddq  7792  caucvgprprlem1  7793  caucvgprprlem2  7794  caucvgsrlemcau  7877  caucvgsrlemgt1  7879  caucvgsrlemoffcau  7882  caucvgsrlemoffres  7884  caucvgsr  7886  axcaucvglemval  7981  axcaucvglemcau  7982  axcaucvglemres  7983  fseq1p1m1  10186  4fvwrd4  10232  fvinim0ffz  10334  frecuzrdgg  10525  frecuzrdgsuctlem  10532  seq3val  10569  seqvalcd  10570  seq3p1  10574  seqp1cd  10579  ser3mono  10596  seq3split  10597  seq3caopr2  10602  iseqf1olemkle  10606  iseqf1olemklt  10607  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemmo  10614  iseqf1olemqk  10616  iseqf1olemjpcl  10617  iseqf1olemqpcl  10618  iseqf1olemfvp  10619  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seq3f1olemqsum  10622  seq3f1olemstep  10623  seq3f1oleml  10625  seq3f1o  10626  seqf1oglem2a  10627  seqf1oglem1  10628  seqf1oglem2  10629  seq3z  10637  seq3distr  10641  ser3ge0  10645  ser3le  10646  exp3vallem  10649  exp3val  10650  bcval5  10872  hashfz1  10892  resunimafz0  10940  leisorel  10946  zfz1isolemiso  10948  seq3coll  10951  caucvgrelemcau  11162  caucvgre  11163  cvg1nlemf  11165  cvg1nlemcau  11166  cvg1nlemres  11167  recvguniqlem  11176  resqrexlemdecn  11194  resqrexlemcalc3  11198  resqrexlemnmsq  11199  resqrexlemnm  11200  resqrexlemcvg  11201  resqrexlemoverl  11203  resqrexlemglsq  11204  resqrexlemga  11205  clim2ser  11519  clim2ser2  11520  climrecvg1n  11530  climcvg1nlem  11531  serf0  11534  sumeq2  11541  fsum3cvg  11560  summodclem2a  11563  fsum3  11569  fisumss  11574  fsumcl2lem  11580  fsumadd  11588  fsummulc2  11630  fsumrelem  11653  isumshft  11672  cvgratnnlemseq  11708  cvgratnnlemrate  11712  clim2prod  11721  clim2divap  11722  prodfrecap  11728  prodfdivap  11729  ntrivcvgap  11730  prodeq2  11739  fproddccvg  11754  prodmodclem3  11757  prodmodclem2a  11758  fprodseq  11765  fprodssdc  11772  fprodmul  11773  effsumlt  11874  nninfctlemfo  12232  nn0seqcvgd  12234  ialgrlem1st  12235  eulerthlemrprm  12422  eulerthlema  12423  eulerthlemh  12424  pcmpt2  12538  pcmptdvds  12539  1arithlem4  12560  1arith  12561  ennnfonelemdc  12641  ennnfonelemjn  12644  ennnfonelemg  12645  ennnfonelemp1  12648  ennnfonelemom  12650  ennnfonelemhdmp1  12651  ennnfonelemss  12652  ennnfonelemkh  12654  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemhom  12657  ennnfonelemnn0  12664  ennnfonelemim  12666  ctinfomlemom  12669  ctiunctlemudc  12679  ctiunctlemf  12680  ctiunctlemfo  12681  ssnnctlemct  12688  nninfdclemp1  12692  nninfdclemlt  12693  imasmnd2  13154  mhmf1o  13172  mhmco  13192  gsumfzcl  13201  isgrpinv  13256  pwssub  13315  imasgrp2  13316  mhmid  13321  mhmmnd  13322  ghmgrp  13324  mulgval  13328  mulgfng  13330  mulgnnsubcl  13340  ghmid  13455  ghminv  13456  ghmmulg  13462  ghmnsgpreima  13475  ghmeqker  13477  ghmf1  13479  kerf1ghm  13480  ghmf1o  13481  imasring  13696  rhmopp  13808  lspcl  14023  znidomb  14290  znrrg  14292  psrbaglesuppg  14302  iscnp4  14538  cnptopco  14542  lmtopcnp  14570  upxp  14592  uptx  14594  txlm  14599  comet  14819  metcnp3  14831  metcnp  14832  metcnp2  14833  metcnpi3  14837  elcncf2  14894  cncfco  14911  ivthreinc  14965  limcimolemlt  14984  cnplimcim  14987  cnplimclemle  14988  cnplimclemr  14989  limccnpcntop  14995  dvlemap  15000  dvcnp2cntop  15019  dvaddxxbr  15021  dvmulxxbr  15022  dvcoapbr  15027  dvcjbr  15028  dvef  15047  plyaddlem1  15067  plymullem1  15068  plycoeid3  15077  plycolemc  15078  plycjlemc  15080  plycj  15081  plycn  15082  plyrecj  15083  dvply1  15085  dvply2g  15086  lgsval  15329  lgscllem  15332  lgsval2lem  15335  lgsval4a  15347  lgsneg  15349  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  lgsne0  15363  lgseisenlem3  15397  lgseisenlem4  15398  1dom1el  15721  2omap  15726  pwle2  15729  subctctexmid  15731  nnsf  15736  peano4nninf  15737  nninfalllem1  15739  nninfsellemdc  15741  nninfsellemeq  15745  nninfsellemqall  15746  nninfsellemeqinf  15747  nninfomnilem  15749  isomninnlem  15761  trilpolemeq1  15771  trilpolemlt1  15772  iswomninnlem  15780  iswomni0  15782  ismkvnnlem  15783  nconstwlpolemgt0  15795  nconstwlpolem  15796