Theorem funfn

Description: A class is a function if and only if it is a function on its domain. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	funfn	⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ dom 𝐴 = dom 𝐴
2	1	biantru	⊢ ( Fun 𝐴 ↔ ( Fun 𝐴 ∧ dom 𝐴 = dom 𝐴 ) )
3		df-fn	⊢ ( 𝐴 Fn dom 𝐴 ↔ ( Fun 𝐴 ∧ dom 𝐴 = dom 𝐴 ) )
4	2 3	bitr4i	⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )