Description: Set of objects of the category of rings (in a universe). (Contributed by AV, 13-Feb-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringcbasALTV.c | |
|
ringcbasALTV.b | |
||
ringcbasALTV.u | |
||
Assertion | ringcbasALTV | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringcbasALTV.c | |
|
2 | ringcbasALTV.b | |
|
3 | ringcbasALTV.u | |
|
4 | eqidd | |
|
5 | eqidd | |
|
6 | eqidd | |
|
7 | 1 3 4 5 6 | ringcvalALTV | |
8 | catstr | |
|
9 | baseid | |
|
10 | snsstp1 | |
|
11 | inex1g | |
|
12 | 3 11 | syl | |
13 | 7 8 9 10 12 2 | strfv3 | |