Theorem ffvelcdmd 5815

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

Syntax hints:   → wi 4   ∈ wcel 2205  ⟶wf 5350  ‘cfv 5354

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4230  ax-pow 4289  ax-pr 4324

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-rex 2528  df-v 2817  df-sbc 3045  df-un 3217  df-in 3219  df-ss 3226  df-pw 3673  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-opab 4174  df-id 4416  df-xp 4757  df-rel 4758  df-cnv 4759  df-co 4760  df-dm 4761  df-rn 4762  df-iota 5314  df-fun 5356  df-fn 5357  df-f 5358  df-fv 5362

This theorem is referenced by:  isotr  5991  caofinvl  6294  fvdifsuppst  6446  rdgon  6619  frecabcl  6632  1dom1el  7062  phplem4dom  7118  fidceq  7126  dif1en  7138  fin0  7144  fin0or  7145  infm  7166  en2eqpr  7169  fidcenumlemrks  7225  fidcenumlemr  7227  2omap  7271  supisoti  7303  ordiso2  7328  updjudhcoinlf  7373  updjudhcoinrg  7374  caseinl  7384  caseinr  7385  difinfsnlem  7392  difinfsn  7393  ctmlemr  7401  ctssdclemn0  7403  ctssdc  7406  enumctlemm  7407  enumct  7408  nnnninfeq2  7422  nninfisol  7426  enomnilem  7431  finomni  7433  ismkvnex  7448  enmkvlem  7454  enwomnilem  7462  nninfwlpoimlemg  7468  nninfwlpoimlemginf  7469  pr2cv1  7494  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  acnccim  7591  cauappcvgprlemm  7965  cauappcvgprlemdisj  7971  cauappcvgprlemloc  7972  cauappcvgprlemladdfu  7974  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  cauappcvgprlem1  7979  cauappcvgprlem2  7980  caucvgprlemnkj  7986  caucvgprlemnbj  7987  caucvgprlemm  7988  caucvgprlemloc  7995  caucvgprlemladdfu  7997  caucvgprlemladdrl  7998  caucvgprlem1  7999  caucvgprlem2  8000  caucvgprprlemnkltj  8009  caucvgprprlemnkeqj  8010  caucvgprprlemnbj  8013  caucvgprprlemmu  8015  caucvgprprlemopl  8017  caucvgprprlemloc  8023  caucvgprprlemexbt  8026  caucvgprprlemexb  8027  caucvgprprlemaddq  8028  caucvgprprlem1  8029  caucvgprprlem2  8030  caucvgsrlemcau  8113  caucvgsrlemgt1  8115  caucvgsrlemoffcau  8118  caucvgsrlemoffres  8120  caucvgsr  8122  axcaucvglemval  8217  axcaucvglemcau  8218  axcaucvglemres  8219  fseq1p1m1  10435  4fvwrd4  10481  fvinim0ffz  10594  frecuzrdgg  10785  frecuzrdgsuctlem  10792  seq3val  10829  seqvalcd  10830  seq3p1  10834  seqp1cd  10839  ser3mono  10856  seq3split  10857  seq3caopr2  10862  iseqf1olemkle  10866  iseqf1olemklt  10867  iseqf1olemqcl  10868  iseqf1olemnab  10870  iseqf1olemmo  10874  iseqf1olemqk  10876  iseqf1olemjpcl  10877  iseqf1olemqpcl  10878  iseqf1olemfvp  10879  seq3f1olemqsumkj  10880  seq3f1olemqsumk  10881  seq3f1olemqsum  10882  seq3f1olemstep  10883  seq3f1oleml  10885  seq3f1o  10886  seqf1oglem2a  10887  seqf1oglem1  10888  seqf1oglem2  10889  seq3z  10897  seq3distr  10901  ser3ge0  10905  ser3le  10906  exp3vallem  10909  exp3val  10910  bcval5  11133  hashfz1  11154  resunimafz0  11206  leisorel  11217  zfz1isolemiso  11219  seq3coll  11222  ccatcl  11289  swrdclg  11350  caucvgrelemcau  11673  caucvgre  11674  cvg1nlemf  11676  cvg1nlemcau  11677  cvg1nlemres  11678  recvguniqlem  11687  resqrexlemdecn  11705  resqrexlemcalc3  11709  resqrexlemnmsq  11710  resqrexlemnm  11711  resqrexlemcvg  11712  resqrexlemoverl  11714  resqrexlemglsq  11715  resqrexlemga  11716  clim2ser  12030  clim2ser2  12031  climrecvg1n  12041  climcvg1nlem  12042  serf0  12045  sumeq2  12052  fsum3cvg  12072  summodclem2a  12075  fsum3  12081  fisumss  12086  fsumcl2lem  12092  fsumadd  12100  fsummulc2  12142  fsumrelem  12165  isumshft  12184  cvgratnnlemseq  12220  cvgratnnlemrate  12224  clim2prod  12233  clim2divap  12234  prodfrecap  12240  prodfdivap  12241  ntrivcvgap  12242  prodeq2  12251  fproddccvg  12266  prodmodclem3  12269  prodmodclem2a  12270  fprodseq  12277  fprodssdc  12284  fprodmul  12285  effsumlt  12386  nninfctlemfo  12744  nn0seqcvgd  12746  ialgrlem1st  12747  eulerthlemrprm  12934  eulerthlema  12935  eulerthlemh  12936  pcmpt2  13050  pcmptdvds  13051  1arithlem4  13072  1arith  13073  ennnfonelemdc  13171  ennnfonelemjn  13174  ennnfonelemg  13175  ennnfonelemp1  13178  ennnfonelemom  13180  ennnfonelemhdmp1  13181  ennnfonelemss  13182  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemex  13186  ennnfonelemhom  13187  ennnfonelemnn0  13194  ennnfonelemim  13196  ctinfomlemom  13199  ctiunctlemudc  13209  ctiunctlemf  13210  ctiunctlemfo  13211  ssnnctlemct  13218  nninfdclemp1  13222  nninfdclemlt  13223  imasmnd2  13686  mhmf1o  13704  mhmco  13724  gsumfzcl  13733  isgrpinv  13788  pwssub  13847  imasgrp2  13848  mhmid  13853  mhmmnd  13854  ghmgrp  13856  mulgval  13860  mulgfng  13862  mulgnnsubcl  13872  ghmid  13987  ghminv  13988  ghmmulg  13994  ghmnsgpreima  14007  ghmeqker  14009  ghmf1  14011  kerf1ghm  14012  ghmf1o  14013  gsumsplit0  14084  imasring  14229  rhmopp  14343  lspcl  14588  znidomb  14855  znrrg  14857  psrbaglesuppg  14870  psrbagfi  14872  psrbaglecl  14873  psrbagcon  14875  mplsubgfilemcl  14903  iscnp4  15132  cnptopco  15136  lmtopcnp  15164  upxp  15186  uptx  15188  txlm  15193  comet  15413  metcnp3  15425  metcnp  15426  metcnp2  15427  metcnpi3  15431  elcncf2  15488  cncfco  15505  ivthreinc  15559  limcimolemlt  15578  cnplimcim  15581  cnplimclemle  15582  cnplimclemr  15583  limccnpcntop  15589  dvlemap  15594  dvcnp2cntop  15613  dvaddxxbr  15615  dvmulxxbr  15616  dvcoapbr  15621  dvcjbr  15622  dvef  15641  plyaddlem1  15661  plymullem1  15662  plycoeid3  15671  plycolemc  15672  plycjlemc  15674  plycj  15675  plycn  15676  plyrecj  15677  dvply1  15679  dvply2g  15680  lgsval  15926  lgscllem  15929  lgsval2lem  15932  lgsval4a  15944  lgsneg  15946  lgsdir  15957  lgsdilem2  15958  lgsdi  15959  lgsne0  15960  lgseisenlem3  15994  lgseisenlem4  15995  p1evtxdeqfi  16356  wlkvtxm  16384  wlkvtxiedg  16389  wlkvtxiedgg  16390  upgriswlkdc  16404  trlsegvdeglem7  16510  trlsegvdegfi  16511  eupth2lem3lem1fi  16512  eupth2lem3lem2fi  16513  eupth2lem3lem3fi  16514  eupth2lem3lem6fi  16515  eupth2lem3lem4fi  16517  eupth2lem3lem7fi  16518  eupth2lemsfi  16522  3dom  16811  pwle2  16821  subctctexmid  16823  nnsf  16832  peano4nninf  16833  nninfalllem1  16835  nninfsellemdc  16837  nninfsellemeq  16841  nninfsellemqall  16842  nninfsellemeqinf  16843  nninfomnilem  16845  nnnninfex  16849  nninfnfiinf  16850  repiecelem  16858  repiecele0  16859  repiecege0  16860  isomninnlem  16863  trilpolemeq1  16873  trilpolemlt1  16874  iswomninnlem  16883  iswomni0  16885  ismkvnnlem  16886  nconstwlpolemgt0  16899  nconstwlpolem  16900  gfsumval  16911  gfsumcl  16919