Theorem grpsubcl

Description: Closure of group subtraction. (Contributed by NM, 31-Mar-2014)

	Ref	Expression
Hypotheses	grpsubcl.b	|- B = ( Base ` G )
	grpsubcl.m	|- .- = ( -g ` G )
Assertion	grpsubcl	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) e. B )

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	|- B = ( Base ` G )
2		grpsubcl.m	|- .- = ( -g ` G )
3	1 2	grpsubf	|- ( G e. Grp -> .- : ( B X. B ) --> B )
4		fovrn	|- ( ( .- : ( B X. B ) --> B /\ X e. B /\ Y e. B ) -> ( X .- Y ) e. B )
5	3 4	syl3an1	|- ( ( G e. Grp /\ X e. B /\ Y e. B ) -> ( X .- Y ) e. B )