Metamath Proof Explorer

Theorem f002

Description: A function with an empty codomain must have empty domain. (Contributed by Zhi Wang, 1-Oct-2024)

Ref Expression
Hypothesis f002.1 
|- ( ph -> F : A --> B )
Assertion f002 
|- ( ph -> ( B = (/) -> A = (/) ) )

Proof

Step Hyp Ref Expression
1 f002.1 
 |-  ( ph -> F : A --> B )
2 feq3 
 |-  ( B = (/) -> ( F : A --> B <-> F : A --> (/) ) )
3 f00 
 |-  ( F : A --> (/) <-> ( F = (/) /\ A = (/) ) )
4 3 simprbi 
 |-  ( F : A --> (/) -> A = (/) )
5 2 4 biimtrdi 
 |-  ( B = (/) -> ( F : A --> B -> A = (/) ) )
6 1 5 syl5com 
 |-  ( ph -> ( B = (/) -> A = (/) ) )