Step | Hyp | Ref
| Expression |
1 | | cdiv 8628 |
. 2
class
/ |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | cc 7808 |
. . 3
class
โ |
5 | | cc0 7810 |
. . . . 5
class
0 |
6 | 5 | csn 3592 |
. . . 4
class
{0} |
7 | 4, 6 | cdif 3126 |
. . 3
class (โ
โ {0}) |
8 | 3 | cv 1352 |
. . . . . 6
class ๐ฆ |
9 | | vz |
. . . . . . 7
setvar ๐ง |
10 | 9 | cv 1352 |
. . . . . 6
class ๐ง |
11 | | cmul 7815 |
. . . . . 6
class
ยท |
12 | 8, 10, 11 | co 5874 |
. . . . 5
class (๐ฆ ยท ๐ง) |
13 | 2 | cv 1352 |
. . . . 5
class ๐ฅ |
14 | 12, 13 | wceq 1353 |
. . . 4
wff (๐ฆ ยท ๐ง) = ๐ฅ |
15 | 14, 9, 4 | crio 5829 |
. . 3
class
(โฉ๐ง
โ โ (๐ฆ ยท
๐ง) = ๐ฅ) |
16 | 2, 3, 4, 7, 15 | cmpo 5876 |
. 2
class (๐ฅ โ โ, ๐ฆ โ (โ โ {0})
โฆ (โฉ๐ง
โ โ (๐ฆ ยท
๐ง) = ๐ฅ)) |
17 | 1, 16 | wceq 1353 |
1
wff / = (๐ฅ โ โ, ๐ฆ โ (โ โ {0})
โฆ (โฉ๐ง
โ โ (๐ฆ ยท
๐ง) = ๐ฅ)) |