This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ffrnb

Description: Characterization of a function with domain and codomain (essentially using that the range is always included in the codomain). Generalization of ffrn . (Contributed by BJ, 21-Sep-2024)

Ref Expression
Assertion ffrnb ⊢ F : A ⟶ B ↔ F : A ⟶ ran ⁡ F ∧ ran ⁡ F ⊆ B

Proof

Step Hyp Ref Expression
1 df-f ⊢ F : A ⟶ B ↔ F Fn A ∧ ran ⁡ F ⊆ B
2 dffn3 ⊢ F Fn A ↔ F : A ⟶ ran ⁡ F
3 2 anbi1i ⊢ F Fn A ∧ ran ⁡ F ⊆ B ↔ F : A ⟶ ran ⁡ F ∧ ran ⁡ F ⊆ B
4 1 3 bitri ⊢ F : A ⟶ B ↔ F : A ⟶ ran ⁡ F ∧ ran ⁡ F ⊆ B