Metamath Proof Explorer

Theorem mof0ALT

Description: Alternate proof for mof0 with stronger requirements on distinct variables. Uses mo4 . (Contributed by Zhi Wang, 19-Sep-2024) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 f00 
 |-  ( f : A --> (/) <-> ( f = (/) /\ A = (/) ) )
2 1 simplbi 
 |-  ( f : A --> (/) -> f = (/) )
3 f00 
 |-  ( g : A --> (/) <-> ( g = (/) /\ A = (/) ) )
4 3 simplbi 
 |-  ( g : A --> (/) -> g = (/) )
5 eqtr3 
 |-  ( ( f = (/) /\ g = (/) ) -> f = g )
6 2 4 5 syl2an 
 |-  ( ( f : A --> (/) /\ g : A --> (/) ) -> f = g )
7 6 gen2 
 |-  A. f A. g ( ( f : A --> (/) /\ g : A --> (/) ) -> f = g )
8 feq1 
 |-  ( f = g -> ( f : A --> (/) <-> g : A --> (/) ) )
9 8 mo4 
 |-  ( E* f f : A --> (/) <-> A. f A. g ( ( f : A --> (/) /\ g : A --> (/) ) -> f = g ) )
10 7 9 mpbir 
 |-  E* f f : A --> (/)