Metamath Proof Explorer

Theorem dffn3

Description: A function maps to its range. (Contributed by NM, 1-Sep-1999)

Ref Expression
Assertion dffn3 ⊢ F Fn A ↔ F : A ⟶ ran ⁡ F

Proof

Step Hyp Ref Expression
1 ssid ⊢ ran ⁡ F ⊆ ran ⁡ F
2 1 biantru ⊢ F Fn A ↔ F Fn A ∧ ran ⁡ F ⊆ ran ⁡ F
3 df-f ⊢ F : A ⟶ ran ⁡ F ↔ F Fn A ∧ ran ⁡ F ⊆ ran ⁡ F
4 2 3 bitr4i ⊢ F Fn A ↔ F : A ⟶ ran ⁡ F