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 | |
|
oppgbas.2 | |
||
Assertion | oppgbasOLD | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oppgbas.1 | |
|
2 | oppgbas.2 | |
|
3 | df-base | |
|
4 | 1nn | |
|
5 | 1ne2 | |
|
6 | 1 3 4 5 | oppglemOLD | |
7 | 2 6 | eqtri | |