Metamath Proof Explorer

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 syl6bi 
 |-  ( 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 syl6bi 
 |-  ( F = (/) -> ( F : X --> Y -> X = (/) ) )
11 10 com12 
 |-  ( F : X --> Y -> ( F = (/) -> X = (/) ) )
12 5 11 impbid 
 |-  ( F : X --> Y -> ( X = (/) <-> F = (/) ) )