Metamath Proof Explorer

Theorem mof0

Description: There is at most one function into the empty set. (Contributed by Zhi Wang, 19-Sep-2024)

Ref Expression
Assertion mof0 
|- E* f f : A --> (/)

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 eqeq2 
 |-  ( g = (/) -> ( f = g <-> f = (/) ) )
3 2 imbi2d 
 |-  ( g = (/) -> ( ( f : A --> (/) -> f = g ) <-> ( f : A --> (/) -> f = (/) ) ) )
4 3 albidv 
 |-  ( g = (/) -> ( A. f ( f : A --> (/) -> f = g ) <-> A. f ( f : A --> (/) -> f = (/) ) ) )
5 1 4 spcev 
 |-  ( A. f ( f : A --> (/) -> f = (/) ) -> E. g A. f ( f : A --> (/) -> f = g ) )
6 f00 
 |-  ( f : A --> (/) <-> ( f = (/) /\ A = (/) ) )
7 6 simplbi 
 |-  ( f : A --> (/) -> f = (/) )
8 5 7 mpg 
 |-  E. g A. f ( f : A --> (/) -> f = g )
9 df-mo 
 |-  ( E* f f : A --> (/) <-> E. g A. f ( f : A --> (/) -> f = g ) )
10 8 9 mpbir 
 |-  E* f f : A --> (/)