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 = ( oppG ` R ) |
|
| oppgbas.2 | |- B = ( Base ` R ) |
||
| Assertion | oppgbasOLD | |- B = ( Base ` O ) |
| 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 | oppglemOLD | |- ( Base ` R ) = ( Base ` O ) |
| 7 | 2 6 | eqtri | |- B = ( Base ` O ) |