Theorem rersubcl

Description: Closure for real subtraction. Based on subcl . (Contributed by Steven Nguyen, 7-Jan-2023)

	Ref	Expression
Assertion	rersubcl	|- ( ( A e. RR /\ B e. RR ) -> ( A -R B ) e. RR )

Proof

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