Theorem f0dom0

Description: A function is empty iff it has an empty domain. (Contributed by AV, 10-Feb-2019)

	Ref	Expression
Assertion	f0dom0	|- ( F : X --> Y -> ( X = (/) <-> F = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		feq2	|- ( X = (/) -> ( F : X --> Y <-> F : (/) --> Y ) )
2		f0bi	|- ( F : (/) --> Y <-> F = (/) )
3	2	biimpi	|- ( F : (/) --> Y -> F = (/) )
4	1 3	biimtrdi	|- ( X = (/) -> ( F : X --> Y -> F = (/) ) )
5	4	com12	|- ( F : X --> Y -> ( X = (/) -> F = (/) ) )
6		feq1	|- ( F = (/) -> ( F : X --> Y <-> (/) : X --> Y ) )
7		fdm	|- ( (/) : X --> Y -> dom (/) = X )
8		dm0	|- dom (/) = (/)
9	7 8	eqtr3di	|- ( (/) : X --> Y -> X = (/) )
10	6 9	biimtrdi	|- ( F = (/) -> ( F : X --> Y -> X = (/) ) )
11	10	com12	|- ( F : X --> Y -> ( F = (/) -> X = (/) ) )
12	5 11	impbid	|- ( F : X --> Y -> ( X = (/) <-> F = (/) ) )