Theorem ffvelcdmda 5717

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 5715	. 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 2176   -->wf 5268   ` cfv 5272

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-14 2179  ax-ext 2187  ax-sep 4163  ax-pow 4219  ax-pr 4254

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ral 2489  df-rex 2490  df-v 2774  df-sbc 2999  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4046  df-opab 4107  df-id 4341  df-xp 4682  df-rel 4683  df-cnv 4684  df-co 4685  df-dm 4686  df-rn 4687  df-iota 5233  df-fun 5274  df-fn 5275  df-f 5276  df-fv 5280

This theorem is referenced by:  ffvelcdmd  5718  f1ocnvdm  5852  foeqcnvco  5861  f1oiso2  5898  offeq  6174  suppssof1  6178  ofco  6179  caofref  6185  caofinvl  6186  caofid0l  6187  caofid0r  6188  caofid1  6189  caofid2  6190  caofcom  6191  caofrss  6192  caoftrn  6193  caofdig  6194  smofvon2dm  6384  smofvon  6387  pw2f1odclem  6933  mapxpen  6947  xpmapenlem  6948  en2eqpr  7006  supisoex  7113  ordiso2  7139  omp1eomlem  7198  ctssdccl  7215  ctssdc  7217  enumctlemm  7218  enomnilem  7242  fodjuomnilemdc  7248  ismkvnex  7259  enmkvlem  7265  enwomnilem  7273  nninfwlporlemd  7276  nninfwlporlem  7277  nninfwlpoimlemginf  7280  cc3  7382  cauappcvgprlemladdru  7771  cauappcvgprlemladdrl  7772  caucvgprlemladdrl  7793  caucvgprprlemopu  7814  caucvgprprlemexbt  7821  caucvgprprlemexb  7822  caucvgsrlemcl  7904  caucvgsrlemfv  7906  caucvgsrlemcau  7908  caucvgsrlembound  7909  caucvgsrlemoffval  7911  caucvgsrlemofff  7912  caucvgsrlemoffgt1  7914  caucvgsrlemoffres  7915  caucvgsr  7917  axcaucvglemcl  8010  ofnegsub  9037  frecuzrdgfunlem  10566  monoord2  10633  seq3f1o  10664  seqf1oglem2  10667  seqf1og  10668  seq3homo  10674  seqfeq3  10676  zfz1isolemiso  10986  seq3coll  10989  wrdsymbcl  11010  ccatcl  11052  resqrexlemfp1  11353  resqrexlemover  11354  resqrexlemdec  11355  resqrexlemlo  11357  resqrexlemcalc1  11358  resqrexlemcalc2  11359  resqrexlemcalc3  11360  resqrexlemgt0  11364  resqrexlemsqa  11368  clim2ser  11681  clim2ser2  11682  isermulc2  11684  iserle  11686  climserle  11689  climrecvg1n  11692  climcvg1nlem  11693  summodclem3  11724  summodclem2a  11725  fsumgcl  11730  fsum3  11731  fsumf1o  11734  isumss  11735  fisumss  11736  fsumcl2lem  11742  fsumadd  11750  isumclim3  11767  isummulc2  11770  isumrecl  11773  isumadd  11775  fsummulc2  11792  iserabs  11819  cvgcmpub  11820  isumshft  11834  isumsplit  11835  mertensabs  11881  clim2prod  11883  clim2divap  11884  prodfap0  11889  prodfdivap  11891  prodmodclem3  11919  prodmodclem2a  11920  fprodseq  11927  fprodf1o  11932  prodssdc  11933  fprodssdc  11934  fprodmul  11935  efcj  12017  nninfctlemfo  12394  nn0seqcvgd  12396  algrp1  12401  alginv  12402  algcvg  12403  algcvga  12406  algfx  12407  eucalgcvga  12413  eulerthlem1  12582  eulerthlemh  12586  eulerthlemth  12587  pcmptcl  12698  pcmpt  12699  1arithlem4  12722  nninfdclemf1  12856  prdsplusgsgrpcl  13279  prdssgrpd  13280  prdsplusgcl  13311  prdsidlem  13312  prdsmndd  13313  gsumwsubmcl  13361  gsumwmhm  13363  grpinvcl  13413  prdsinvlem  13473  pwsinvg  13477  pwssub  13478  mhmmulg  13532  ghminv  13619  gsumfzreidx  13706  gsumfzsubmcl  13707  gsumfzmptfidmadd  13708  gsumfzmhm  13712  rhmdvdsr  13970  psrlinv  14479  psr1clfi  14483  mplsubgfilemcl  14494  cnptoprest2  14745  lmss  14751  txcnmpt  14778  txlm  14784  lmcn2  14785  psmetxrge0  14837  metcnp  15017  climcncf  15089  negfcncf  15111  ivthdec  15149  ivthreinc  15150  dvcnp2cntop  15204  dvaddxxbr  15206  dvimulf  15211  dvcj  15214  dvfre  15215  elply2  15240  plyaddlem1  15252  plymullem1  15253  plycolemc  15263  plyco  15264  dvply2g  15271  lgscllem  15517  lgsfle1  15519  lgsval4a  15532  lgsneg  15534  lgsdir  15545  lgsdilem2  15546  lgsdi  15547  lgsne0  15548  nninfall  15983  nninffeq  15994  refeq  16004  trilpolemclim  16012  trilpolemcl  16013  trilpolemisumle  16014  trilpolemeq1  16016  iswomni0  16027