Theorem sn-subcl

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

	Ref	Expression
Assertion	sn-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		sn-subeu	|- ( ( 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 )