Theorem grpinvcl

Description: A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 4-May-2015)

	Ref	Expression
Hypotheses	grpinvcl.b	|- B = ( Base ` G )
	grpinvcl.n	|- N = ( invg ` G )
Assertion	grpinvcl	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )

Proof

Step	Hyp	Ref	Expression
1		grpinvcl.b	|- B = ( Base ` G )
2		grpinvcl.n	|- N = ( invg ` G )
3	1 2	grpinvf	|- ( G e. Grp -> N : B --> B )
4	3	ffvelrnda	|- ( ( G e. Grp /\ X e. B ) -> ( N ` X ) e. B )