Theorem f0cli

Description: Unconditional closure of a function when the range includes the empty set. (Contributed by Mario Carneiro, 12-Sep-2013)

	Ref	Expression
Hypotheses	f0cl.1	|- F : A --> B
	f0cl.2	|- (/) e. B
Assertion	f0cli	|- ( F ` C ) e. B

Proof

Step	Hyp	Ref	Expression
1		f0cl.1	|- F : A --> B
2		f0cl.2	|- (/) e. B
3	1	ffvelrni	|- ( C e. A -> ( F ` C ) e. B )
4	1	fdmi	|- dom F = A
5	4	eleq2i	|- ( C e. dom F <-> C e. A )
6		ndmfv	|- ( -. C e. dom F -> ( F ` C ) = (/) )
7	6 2	eqeltrdi	|- ( -. C e. dom F -> ( F ` C ) e. B )
8	5 7	sylnbir	|- ( -. C e. A -> ( F ` C ) e. B )
9	3 8	pm2.61i	|- ( F ` C ) e. B