Metamath Proof Explorer

Theorem dffn4

Description: A function maps onto its range. (Contributed by NM, 10-May-1998)

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

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ F = ran ⁡ F
2 1 biantru ⊢ F Fn A ↔ F Fn A ∧ ran ⁡ F = ran ⁡ F
3 df-fo ⊢ F : A ⟶ onto ran ⁡ F ↔ F Fn A ∧ ran ⁡ F = ran ⁡ F
4 2 3 bitr4i ⊢ F Fn A ↔ F : A ⟶ onto ran ⁡ F