Theorem rrgss

Description: Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015)

	Ref	Expression
Hypotheses	rrgss.e	|- E = ( RLReg ` R )
	rrgss.b	|- B = ( Base ` R )
Assertion	rrgss	|- E C_ B

Proof

Step	Hyp	Ref	Expression
1		rrgss.e	|- E = ( RLReg ` R )
2		rrgss.b	|- B = ( Base ` R )
3		eqid	|- ( .r ` R ) = ( .r ` R )
4		eqid	|- ( 0g ` R ) = ( 0g ` R )
5	1 2 3 4	rrgval	|- E = { x e. B | A. y e. B ( ( x ( .r ` R ) y ) = ( 0g ` R ) -> y = ( 0g ` R ) ) }
6	5	ssrab3	|- E C_ B