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

Metamath Proof Explorer

Theorem funforn

Description: A function maps its domain onto its range. (Contributed by NM, 23-Jul-2004)

Ref Expression
Assertion funforn ⊢ Fun ⁡ A ↔ A : dom ⁡ A ⟶ onto ran ⁡ A

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ A ↔ A Fn dom ⁡ A
2 dffn4 ⊢ A Fn dom ⁡ A ↔ A : dom ⁡ A ⟶ onto ran ⁡ A
3 1 2 bitri ⊢ Fun ⁡ A ↔ A : dom ⁡ A ⟶ onto ran ⁡ A