Theorem ffvelrn 5593

Description: A function's value belongs to its codomain. (Contributed by NM, 12-Aug-1999.)

Assertion

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

Proof of Theorem ffvelrn

Step	Hyp	Ref	Expression
1		ffn 5312	. . 3 |- ( F : A --> B -> F Fn A )
2		fnfvelrn 5592	. . 3 |- ( ( F Fn A /\ C e. A ) -> ( F ` C ) e. ran F )
3	1, 2	sylan 281	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. ran F )
4		frn 5321	. . . 4 |- ( F : A --> B -> ran F C_ B )
5	4	sseld 3123	. . 3 |- ( F : A --> B -> ( ( F ` C ) e. ran F -> ( F ` C ) e. B ) )
6	5	adantr 274	. 2 |- ( ( F : A --> B /\ C e. A ) -> ( ( F ` C ) e. ran F -> ( F ` C ) e. B ) )
7	3, 6	mpd 13	1 |- ( ( F : A --> B /\ C e. A ) -> ( F ` C ) e. B )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 2125   ran crn 4580   Fn wfn 5158   -->wf 5159   ` cfv 5163

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 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-pow 4130  ax-pr 4164

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-rex 2438  df-v 2711  df-sbc 2934  df-un 3102  df-in 3104  df-ss 3111  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-br 3962  df-opab 4022  df-id 4248  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-fv 5171

This theorem is referenced by:  ffvelrni  5594  ffvelrnda  5595  dffo3  5607  ffnfv  5618  ffvresb  5623  fcompt  5630  fsn2  5634  fvconst  5648  foco2  5695  fcofo  5725  cocan1  5728  isocnv  5752  isores2  5754  isopolem  5763  isosolem  5765  fovrn  5953  off  6034  mapsncnv  6629  2dom  6739  enm  6754  xpdom2  6765  xpmapenlem  6783  fiintim  6862  isotilem  6938  updjudhf  7009  exmidomniim  7063  shftf  10707  summodclem2a  11255  isumcl  11299  mertenslem2  11410  nn0seqcvgd  11889  algrf  11893  eucalg  11907  phimullem  12068  upxp  12611  uptx  12613  txhmeo  12658  cncfmet  12918  dvaddxxbr  13004  dvcj  13012  dvfre  13013  bj-charfunr  13323