Theorem fdmrn

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

	Ref	Expression
Assertion	fdmrn	⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ran 𝐹 ⊆ ran 𝐹
2		df-f	⊢ ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ ran 𝐹 ) )
3	1 2	mpbiran2	⊢ ( 𝐹 : dom 𝐹 ⟶ ran 𝐹 ↔ 𝐹 Fn dom 𝐹 )
4		eqid	⊢ dom 𝐹 = dom 𝐹
5		df-fn	⊢ ( 𝐹 Fn dom 𝐹 ↔ ( Fun 𝐹 ∧ dom 𝐹 = dom 𝐹 ) )
6	4 5	mpbiran2	⊢ ( 𝐹 Fn dom 𝐹 ↔ Fun 𝐹 )
7	3 6	bitr2i	⊢ ( Fun 𝐹 ↔ 𝐹 : dom 𝐹 ⟶ ran 𝐹 )