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

Metamath Proof Explorer

Theorem ffrnbd

Description: A function maps to its range iff the range is a subset of its codomain. Generalization of ffrn . (Contributed by AV, 20-Sep-2024)

Ref Expression
Hypothesis ffrnbd.r ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
Assertion ffrnbd ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ffrnbd.r ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝐵 )
2 ffrnb ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) )
3 1 biantrud ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ ran 𝐹 ↔ ( 𝐹 : 𝐴 ⟶ ran 𝐹 ∧ ran 𝐹 ⊆ 𝐵 ) ) )
4 2 3 bitr4id ⊢ ( 𝜑 → ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 ) )