Theorem fdmrn

Description: A different way to write F is a function. (Contributed by Thierry Arnoux, 7-Dec-2016)

	Ref	Expression
Assertion	fdmrn	|- ( Fun F <-> F : dom F --> ran F )

Proof

Step	Hyp	Ref	Expression
1		ssid	|- ran F C_ ran F
2		df-f	|- ( F : dom F --> ran F <-> ( F Fn dom F /\ ran F C_ ran F ) )
3	1 2	mpbiran2	|- ( F : dom F --> ran F <-> F Fn dom F )
4		eqid	|- dom F = dom F
5		df-fn	|- ( F Fn dom F <-> ( Fun F /\ dom F = dom F ) )
6	4 5	mpbiran2	|- ( F Fn dom F <-> Fun F )
7	3 6	bitr2i	|- ( Fun F <-> F : dom F --> ran F )