Metamath Proof Explorer

Theorem fnfvrnss

Description: An upper bound for range determined by function values. (Contributed by NM, 8-Oct-2004)

Ref Expression
Assertion fnfvrnss 
|- ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )

Proof

Step Hyp Ref Expression
1 ffnfv 
 |-  ( F : A --> B <-> ( F Fn A /\ A. x e. A ( F ` x ) e. B ) )
2 frn 
 |-  ( F : A --> B -> ran F C_ B )
3 1 2 sylbir 
 |-  ( ( F Fn A /\ A. x e. A ( F ` x ) e. B ) -> ran F C_ B )