Metamath Proof Explorer


Theorem sn-negex2

Description: Proof of cnegex2 without ax-mulcom . (Contributed by SN, 5-May-2024)

Ref Expression
Assertion sn-negex2
|- ( A e. CC -> E. b e. CC ( b + A ) = 0 )

Proof

Step Hyp Ref Expression
1 sn-negex12
 |-  ( A e. CC -> E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) )
2 simpr
 |-  ( ( ( A + b ) = 0 /\ ( b + A ) = 0 ) -> ( b + A ) = 0 )
3 2 reximi
 |-  ( E. b e. CC ( ( A + b ) = 0 /\ ( b + A ) = 0 ) -> E. b e. CC ( b + A ) = 0 )
4 1 3 syl
 |-  ( A e. CC -> E. b e. CC ( b + A ) = 0 )