Theorem grpodivcl

Description: Closure of group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdivf.1	|- X = ran G
	grpdivf.3	|- D = ( /g ` G )
Assertion	grpodivcl	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) e. X )

Proof

Step	Hyp	Ref	Expression
1		grpdivf.1	|- X = ran G
2		grpdivf.3	|- D = ( /g ` G )
3	1 2	grpodivf	|- ( G e. GrpOp -> D : ( X X. X ) --> X )
4		fovrn	|- ( ( D : ( X X. X ) --> X /\ A e. X /\ B e. X ) -> ( A D B ) e. X )
5	3 4	syl3an1	|- ( ( G e. GrpOp /\ A e. X /\ B e. X ) -> ( A D B ) e. X )