Theorem ffvelcdmd 5847

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2209  ⟶wf 5376  ‘cfv 5380

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-iota 5340  df-fun 5382  df-fn 5383  df-f 5384  df-fv 5388

This theorem is used by:  isotr  6025  caofinvl  6332  fvdifsuppst  6488  rdgon  6661  frecabcl  6674  1dom1el  7112  phplem4dom  7168  fidceq  7176  dif1en  7188  fin0  7194  fin0or  7195  infm  7216  en2eqpr  7219  fidcenumlemrks  7276  fidcenumlemr  7278  fdcf1  7322  2omap  7325  supisoti  7357  ordiso2  7382  updjudhcoinlf  7427  updjudhcoinrg  7428  caseinl  7438  caseinr  7439  difinfsnlem  7446  difinfsn  7447  ctmlemr  7455  ctssdclemn0  7457  ctssdc  7460  enumctlemm  7461  enumct  7462  nnnninfeq2  7476  nninfisol  7480  enomnilem  7485  finomni  7487  ismkvnex  7502  enmkvlem  7508  enwomnilem  7516  nninfwlpoimlemg  7522  nninfwlpoimlemginf  7523  pr2cv1  7548  exmidfodomrlemr  7561  exmidfodomrlemrALT  7562  acnccim  7645  cauappcvgprlemm  8019  cauappcvgprlemdisj  8025  cauappcvgprlemloc  8026  cauappcvgprlemladdfu  8028  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  cauappcvgprlem1  8033  cauappcvgprlem2  8034  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemm  8042  caucvgprlemloc  8049  caucvgprlemladdfu  8051  caucvgprlemladdrl  8052  caucvgprlem1  8053  caucvgprlem2  8054  caucvgprprlemnkltj  8063  caucvgprprlemnkeqj  8064  caucvgprprlemnbj  8067  caucvgprprlemmu  8069  caucvgprprlemopl  8071  caucvgprprlemloc  8077  caucvgprprlemexbt  8080  caucvgprprlemexb  8081  caucvgprprlemaddq  8082  caucvgprprlem1  8083  caucvgprprlem2  8084  caucvgsrlemcau  8167  caucvgsrlemgt1  8169  caucvgsrlemoffcau  8172  caucvgsrlemoffres  8174  caucvgsr  8176  axcaucvglemval  8271  axcaucvglemcau  8272  axcaucvglemres  8273  fseq1p1m1  10519  4fvwrd4  10565  fvinim0ffz  10678  frecuzrdgg  10875  frecuzrdgsuctlem  10882  seq3val  10919  seqvalcd  10920  seq3p1  10924  seqp1cd  10929  ser3mono  10946  seq3split  10947  seq3caopr2  10952  iseqf1olemkle  10956  iseqf1olemklt  10957  iseqf1olemqcl  10958  iseqf1olemnab  10960  iseqf1olemmo  10964  iseqf1olemqk  10966  iseqf1olemjpcl  10967  iseqf1olemqpcl  10968  iseqf1olemfvp  10969  seq3f1olemqsumkj  10970  seq3f1olemqsumk  10971  seq3f1olemqsum  10972  seq3f1olemstep  10973  seq3f1oleml  10975  seq3f1o  10976  seqf1oglem2a  10977  seqf1oglem1  10978  seqf1oglem2  10979  seq3z  10987  seq3distr  10991  ser3ge0  10995  ser3le  10996  exp3vallem  10999  exp3val  11000  bcval5  11224  hashfz1  11245  resunimafz0  11297  leisorel  11312  zfz1isolemiso  11314  seq3coll  11317  ccatcl  11384  swrdclg  11445  caucvgrelemcau  11769  caucvgre  11770  cvg1nlemf  11772  cvg1nlemcau  11773  cvg1nlemres  11774  recvguniqlem  11783  resqrexlemdecn  11801  resqrexlemcalc3  11805  resqrexlemnmsq  11806  resqrexlemnm  11807  resqrexlemcvg  11808  resqrexlemoverl  11810  resqrexlemglsq  11811  resqrexlemga  11812  fiidxsupcl  12019  clim2ser  12129  clim2ser2  12130  climrecvg1n  12140  climcvg1nlem  12141  serf0  12144  sumeq2  12151  fsum3cvg  12171  summodclem2a  12174  fsum3  12180  fisumss  12185  fsumcl2lem  12191  fsumadd  12199  fsummulc2  12241  fsumrelem  12264  isumshft  12283  cvgratnnlemseq  12319  cvgratnnlemrate  12323  clim2prod  12332  clim2divap  12333  prodfrecap  12339  prodfdivap  12340  ntrivcvgap  12341  prodeq2  12350  fproddccvg  12365  prodmodclem3  12368  prodmodclem2a  12369  fprodseq  12376  fprodssdc  12383  fprodmul  12384  effsumlt  12485  nninfctlemfo  12843  nn0seqcvgd  12845  ialgrlem1st  12846  eulerthlemrprm  13037  eulerthlema  13038  eulerthlemh  13039  pcmpt2  13153  pcmptdvds  13154  1arithlem4  13175  1arith  13176  ennnfonelemdc  13349  ennnfonelemjn  13352  ennnfonelemg  13353  ennnfonelemp1  13356  ennnfonelemom  13358  ennnfonelemhdmp1  13359  ennnfonelemss  13360  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemex  13364  ennnfonelemhom  13365  ennnfonelemnn0  13372  ennnfonelemim  13374  ctinfomlemom  13377  ctiunctlemudc  13387  ctiunctlemf  13388  ctiunctlemfo  13389  ssnnctlemct  13396  nninfdclemp1  13400  nninfdclemlt  13401  imasmnd2  13819  mhmf1o  13837  mhmco  13857  gzsumcl  13864  isgrpinv  13919  imasgrp2  13973  mhmid  13978  mhmmnd  13979  ghmgrp  13981  mulgval  13985  mulgfng  13987  mulgnnsubcl  13997  ghmid  14112  ghminv  14113  ghmmulg  14119  ghmnsgpreima  14132  ghmeqker  14134  ghmf1  14136  kerf1ghm  14137  ghmf1o  14138  gzsumsplit0  14239  gsumvalfi  14243  gsumclfi  14250  gsumsubmclfi  14254  gsumresfi  14264  pwssub  14324  imasring  14479  rhmopp  14593  lspcl  14838  znidomb  15103  znrrg  15105  asclelbas  15136  psrbagfi  15168  psrbaglesuppg  15172  psrbaglecl  15174  psrbagcon  15176  psrbaglefifi  15177  rhmpsrfilem2  15190  psrmulvalfi  15193  psrlidmfi  15204  psrridmfi  15205  psrass1fi  15206  psrdifi  15207  psrdirfi  15208  mvrcl2fi  15216  mplsubgfilemcl  15227  iscnp4  15456  cnptopco  15460  lmtopcnp  15488  upxp  15510  uptx  15512  txlm  15517  comet  15737  metcnp3  15749  metcnp  15750  metcnp2  15751  metcnpi3  15755  elcncf2  15812  cncfco  15829  ivthreinc  15883  limcimolemlt  15902  cnplimcim  15905  cnplimclemle  15906  cnplimclemr  15907  limccnpcntop  15913  dvlemap  15918  dvcnp2cntop  15937  dvaddxxbr  15939  dvmulxxbr  15940  dvcoapbr  15945  dvcjbr  15946  dvef  15965  plyaddlem1  15985  plymullem1  15986  plycoeid3  15995  plycolemc  15996  plycjlemc  15998  plycj  15999  plycn  16000  plyrecj  16001  dvply1  16003  dvply2g  16004  logfac  16138  bposlem3  16325  bposlem5  16327  bposlem6  16328  bposlem9  16331  lgsval  16340  lgscllem  16343  lgsval2lem  16346  lgsval4a  16358  lgsneg  16360  lgsdir  16371  lgsdilem2  16372  lgsdi  16373  lgsne0  16374  lgseisenlem3  16408  lgseisenlem4  16409  p1evtxdeqfi  16770  wlkvtxm  16798  wlkvtxiedg  16803  wlkvtxiedgg  16804  upgriswlkdc  16818  trlsegvdeglem7  16924  trlsegvdegfi  16925  eupth2lem3lem1fi  16926  eupth2lem3lem2fi  16927  eupth2lem3lem3fi  16928  eupth2lem3lem6fi  16929  eupth2lem3lem4fi  16931  eupth2lem3lem7fi  16932  eupth2lemsfi  16936  3dom  17235  pwle2  17245  subctctexmid  17247  nnsf  17266  peano4nninf  17267  nninfalllem1  17269  nninfsellemdc  17271  nninfsellemeq  17275  nninfsellemqall  17276  nninfsellemeqinf  17277  nninfomnilem  17279  nnnninfex  17283  nninfnfiinf  17284  repiecelem  17292  repiecele0  17293  repiecege0  17294  isomninnlem  17297  trilpolemeq1  17308  trilpolemlt1  17309  iswomninnlem  17318  iswomni0  17320  ismkvnnlem  17321  nconstwlpolemgt0  17333  nconstwlpolem  17334