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 ∧ ∀ x ∈ A F ⁡ x ∈ B → ran ⁡ F ⊆ B

Proof

Step Hyp Ref Expression
1 ffnfv ⊢ F : A ⟶ B ↔ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B
2 frn ⊢ F : A ⟶ B → ran ⁡ F ⊆ B
3 1 2 sylbir ⊢ F Fn A ∧ ∀ x ∈ A F ⁡ x ∈ B → ran ⁡ F ⊆ B