Theorem ffvelcdmi 5634

Description: A function's value belongs to its codomain. (Contributed by NM, 6-Apr-2005.)

Hypothesis

Ref	Expression
ffvelcdmi.1	|- F : A --> B

Assertion

Ref	Expression
ffvelcdmi	|- ( C e. A -> ( F ` C ) e. B )

Proof of Theorem ffvelcdmi

Step	Hyp	Ref	Expression
1		ffvelcdmi.1	. 2 |- F : A --> B
2		ffvelcdm 5633	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )
3	1, 2	mpan 422	1 |- ( C e. A -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   e. wcel 2142   -->wf 5196   ` cfv 5200

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 705  ax-5 1441  ax-7 1442  ax-gen 1443  ax-ie1 1487  ax-ie2 1488  ax-8 1498  ax-10 1499  ax-11 1500  ax-i12 1501  ax-bndl 1503  ax-4 1504  ax-17 1520  ax-i9 1524  ax-ial 1528  ax-i5r 1529  ax-14 2145  ax-ext 2153  ax-sep 4108  ax-pow 4161  ax-pr 4195

This theorem depends on definitions:  df-bi 116  df-3an 976  df-tru 1352  df-nf 1455  df-sb 1757  df-eu 2023  df-mo 2024  df-clab 2158  df-cleq 2164  df-clel 2167  df-nfc 2302  df-ral 2454  df-rex 2455  df-v 2733  df-sbc 2957  df-un 3126  df-in 3128  df-ss 3135  df-pw 3569  df-sn 3590  df-pr 3591  df-op 3593  df-uni 3798  df-br 3991  df-opab 4052  df-id 4279  df-xp 4618  df-rel 4619  df-cnv 4620  df-co 4621  df-dm 4622  df-rn 4623  df-iota 5162  df-fun 5202  df-fn 5203  df-f 5204  df-fv 5208

This theorem is referenced by:  omgadd  10741  cjcl  10816  climmpt  11267  cn1lem  11281  climcn1lem  11286  fsumrelem  11438  efcl  11631  sincl  11673  coscl  11674  algcvg  12006  algcvgb  12008  algcvga  12009  algfx  12010  eucalgcvga  12016  eucalg  12017  sqpweven  12133  2sqpwodd  12134  ennnfonelemnn0  12381  relogcl  13694  nninfomnilem  14168