Metamath Proof Explorer

Theorem subcl

Description: Closure law for subtraction. (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 21-Dec-2013)

Ref Expression
Assertion subcl 
|- ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )

Proof

Step Hyp Ref Expression
1 subval 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) = ( iota_ x e. CC ( B + x ) = A ) )
2 negeu 
 |-  ( ( B e. CC /\ A e. CC ) -> E! x e. CC ( B + x ) = A )
3 2 ancoms 
 |-  ( ( A e. CC /\ B e. CC ) -> E! x e. CC ( B + x ) = A )
4 riotacl 
 |-  ( E! x e. CC ( B + x ) = A -> ( iota_ x e. CC ( B + x ) = A ) e. CC )
5 3 4 syl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( iota_ x e. CC ( B + x ) = A ) e. CC )
6 1 5 eqeltrd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A - B ) e. CC )