Metamath Proof Explorer

Theorem f0bi

Description: A function with empty domain is empty. (Contributed by Alexander van der Vekens, 30-Jun-2018)

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

Proof

Step Hyp Ref Expression
1 ffn 
 |-  ( F : (/) --> X -> F Fn (/) )
2 fn0 
 |-  ( F Fn (/) <-> F = (/) )
3 1 2 sylib 
 |-  ( F : (/) --> X -> F = (/) )
4 f0 
 |-  (/) : (/) --> X
5 feq1 
 |-  ( F = (/) -> ( F : (/) --> X <-> (/) : (/) --> X ) )
6 4 5 mpbiri 
 |-  ( F = (/) -> F : (/) --> X )
7 3 6 impbii 
 |-  ( F : (/) --> X <-> F = (/) )