Theorem oppgbas

Description: Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015)

	Ref	Expression
Hypotheses	oppgbas.1	|- O = ( oppG ` R )
	oppgbas.2	|- B = ( Base ` R )
Assertion	oppgbas	|- B = ( Base ` O )

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	|- O = ( oppG ` R )
2		oppgbas.2	|- B = ( Base ` R )
3		df-base	|- Base = Slot 1
4		1nn	|- 1 e. NN
5		1ne2	|- 1 =/= 2
6	1 3 4 5	oppglem	|- ( Base ` R ) = ( Base ` O )
7	2 6	eqtri	|- B = ( Base ` O )