Description: Set of objects of the category of non-unital rings (in a universe). (Contributed by AV, 27-Feb-2020) (Revised by AV, 8-Mar-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | rngcbas.c | |
|
rngcbas.b | |
||
rngcbas.u | |
||
Assertion | rngcbas | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rngcbas.c | |
|
2 | rngcbas.b | |
|
3 | rngcbas.u | |
|
4 | eqidd | |
|
5 | eqidd | |
|
6 | 1 3 4 5 | rngcval | |
7 | 6 | fveq2d | |
8 | 2 | a1i | |
9 | eqid | |
|
10 | eqid | |
|
11 | fvexd | |
|
12 | 4 5 | rnghmresfn | |
13 | inss1 | |
|
14 | eqid | |
|
15 | 14 3 | estrcbas | |
16 | 13 15 | sseqtrid | |
17 | 9 10 11 12 16 | rescbas | |
18 | 7 8 17 | 3eqtr4d | |