Description: Set of arrows of the category of rings (in a universe). (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ringcbasALTV.c | |
|
ringcbasALTV.b | |
||
ringcbasALTV.u | |
||
ringchomfvalALTV.h | |
||
ringchomALTV.x | |
||
ringchomALTV.y | |
||
Assertion | ringchomALTV | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ringcbasALTV.c | |
|
2 | ringcbasALTV.b | |
|
3 | ringcbasALTV.u | |
|
4 | ringchomfvalALTV.h | |
|
5 | ringchomALTV.x | |
|
6 | ringchomALTV.y | |
|
7 | 1 2 3 4 | ringchomfvalALTV | |
8 | oveq12 | |
|
9 | 8 | adantl | |
10 | ovexd | |
|
11 | 7 9 5 6 10 | ovmpod | |