Metamath Proof Explorer

Theorem fafvelrn

Description: A function's value belongs to its codomain, analogous to ffvelrn . (Contributed by Alexander van der Vekens, 25-May-2017)

Ref Expression
Assertion fafvelrn 
|- ( ( F : A --> B /\ C e. A ) -> ( F ''' C ) e. B )

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : A --> B -> F Fn A )
2 fnafvelrn 
 |-  ( ( F Fn A /\ C e. A ) -> ( F ''' C ) e. ran F )
3 1 2 sylan 
 |-  ( ( F : A --> B /\ C e. A ) -> ( F ''' C ) e. ran F )
4 frn 
 |-  ( F : A --> B -> ran F C_ B )
5 4 sseld 
 |-  ( F : A --> B -> ( ( F ''' C ) e. ran F -> ( F ''' C ) e. B ) )
6 5 adantr 
 |-  ( ( F : A --> B /\ C e. A ) -> ( ( F ''' C ) e. ran F -> ( F ''' C ) e. B ) )
7 3 6 mpd 
 |-  ( ( F : A --> B /\ C e. A ) -> ( F ''' C ) e. B )