Metamath Proof Explorer


Theorem oppgbasOLD

Description: Obsolete version of oppgbas as of 18-Oct-2024. Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses oppgbas.1 O=opp𝑔R
oppgbas.2 B=BaseR
Assertion oppgbasOLD B=BaseO

Proof

Step Hyp Ref Expression
1 oppgbas.1 O=opp𝑔R
2 oppgbas.2 B=BaseR
3 df-base Base=Slot1
4 1nn 1
5 1ne2 12
6 1 3 4 5 oppglemOLD BaseR=BaseO
7 2 6 eqtri B=BaseO