Theorem ffvelcdmda 5782

Description: A function's value belongs to its codomain. (Contributed by Mario Carneiro, 29-Dec-2016.)

Hypothesis

Ref	Expression
ffvelcdmd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
ffvelcdmda	|- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmda

Step	Hyp	Ref	Expression
1		ffvelcdmd.1	. 2 |- ( ph -> F : A --> B )
2		ffvelcdm 5780	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3	1, 2	sylan 283	1 |- ( ( ph /\ C e. A ) -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2202   -->wf 5322   ` cfv 5326

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-rex 2516  df-v 2804  df-sbc 3032  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-fv 5334

This theorem is referenced by:  ffvelcdmd  5783  f1ocnvdm  5922  foeqcnvco  5931  f1oiso2  5968  offeq  6249  suppssof1  6253  ofco  6254  caofref  6260  caofinvl  6261  caofid0l  6262  caofid0r  6263  caofid1  6264  caofid2  6265  caofcom  6266  caofrss  6267  caoftrn  6268  caofdig  6269  smofvon2dm  6462  smofvon  6465  pw2f1odclem  7020  mapxpen  7034  xpmapenlem  7035  en2eqpr  7099  supisoex  7208  ordiso2  7234  omp1eomlem  7293  ctssdccl  7310  ctssdc  7312  enumctlemm  7313  enomnilem  7337  fodjuomnilemdc  7343  ismkvnex  7354  enmkvlem  7360  enwomnilem  7368  nninfwlporlemd  7371  nninfwlporlem  7372  nninfwlpoimlemginf  7375  cc3  7487  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemopu  7919  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  caucvgsrlemcl  8009  caucvgsrlemfv  8011  caucvgsrlemcau  8013  caucvgsrlembound  8014  caucvgsrlemoffval  8016  caucvgsrlemofff  8017  caucvgsrlemoffgt1  8019  caucvgsrlemoffres  8020  caucvgsr  8022  axcaucvglemcl  8115  ofnegsub  9142  frecuzrdgfunlem  10682  monoord2  10749  seq3f1o  10780  seqf1oglem2  10783  seqf1og  10784  seq3homo  10790  seqfeq3  10792  zfz1isolemiso  11104  seq3coll  11107  wrdsymbcl  11131  ccatcl  11174  resqrexlemfp1  11587  resqrexlemover  11588  resqrexlemdec  11589  resqrexlemlo  11591  resqrexlemcalc1  11592  resqrexlemcalc2  11593  resqrexlemcalc3  11594  resqrexlemgt0  11598  resqrexlemsqa  11602  clim2ser  11915  clim2ser2  11916  isermulc2  11918  iserle  11920  climserle  11923  climrecvg1n  11926  climcvg1nlem  11927  summodclem3  11959  summodclem2a  11960  fsumgcl  11965  fsum3  11966  fsumf1o  11969  isumss  11970  fisumss  11971  fsumcl2lem  11977  fsumadd  11985  isumclim3  12002  isummulc2  12005  isumrecl  12008  isumadd  12010  fsummulc2  12027  iserabs  12054  cvgcmpub  12055  isumshft  12069  isumsplit  12070  mertensabs  12116  clim2prod  12118  clim2divap  12119  prodfap0  12124  prodfdivap  12126  prodmodclem3  12154  prodmodclem2a  12155  fprodseq  12162  fprodf1o  12167  prodssdc  12168  fprodssdc  12169  fprodmul  12170  efcj  12252  nninfctlemfo  12629  nn0seqcvgd  12631  algrp1  12636  alginv  12637  algcvg  12638  algcvga  12641  algfx  12642  eucalgcvga  12648  eulerthlem1  12817  eulerthlemh  12821  eulerthlemth  12822  pcmptcl  12933  pcmpt  12934  1arithlem4  12957  nninfdclemf1  13091  prdsplusgsgrpcl  13515  prdssgrpd  13516  prdsplusgcl  13547  prdsidlem  13548  prdsmndd  13549  gsumwsubmcl  13597  gsumwmhm  13599  grpinvcl  13649  prdsinvlem  13709  pwsinvg  13713  pwssub  13714  mhmmulg  13768  ghminv  13855  gsumfzreidx  13942  gsumfzsubmcl  13943  gsumfzmptfidmadd  13944  gsumfzmhm  13948  rhmdvdsr  14208  psrlinv  14717  psr1clfi  14721  mplsubgfilemcl  14732  cnptoprest2  14983  lmss  14989  txcnmpt  15016  txlm  15022  lmcn2  15023  psmetxrge0  15075  metcnp  15255  climcncf  15327  negfcncf  15349  ivthdec  15387  ivthreinc  15388  dvcnp2cntop  15442  dvaddxxbr  15444  dvimulf  15449  dvcj  15452  dvfre  15453  elply2  15478  plyaddlem1  15490  plymullem1  15491  plycolemc  15501  plyco  15502  dvply2g  15509  lgscllem  15755  lgsfle1  15757  lgsval4a  15770  lgsneg  15772  lgsdir  15783  lgsdilem2  15784  lgsdi  15785  lgsne0  15786  uhgrss  15945  uhgrm  15948  upgrss  15969  upgrm  15970  upgr1or2  15971  umgredg2en  15979  lfgredg2dom  16002  usgrss  16047  depindlem1  16376  depindlem2  16377  pw1map  16647  nninfall  16662  nninffeq  16673  refeq  16683  trilpolemclim  16691  trilpolemcl  16692  trilpolemisumle  16693  trilpolemeq1  16695  iswomni0  16707