Step | Hyp | Ref
| Expression |
1 | | cxdiv 31829 |
. 2
class
/๐ |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | cxr 11196 |
. . 3
class
โ* |
5 | | cr 11058 |
. . . 4
class
โ |
6 | | cc0 11059 |
. . . . 5
class
0 |
7 | 6 | csn 4590 |
. . . 4
class
{0} |
8 | 5, 7 | cdif 3911 |
. . 3
class (โ
โ {0}) |
9 | 3 | cv 1541 |
. . . . . 6
class ๐ฆ |
10 | | vz |
. . . . . . 7
setvar ๐ง |
11 | 10 | cv 1541 |
. . . . . 6
class ๐ง |
12 | | cxmu 13040 |
. . . . . 6
class
ยทe |
13 | 9, 11, 12 | co 7361 |
. . . . 5
class (๐ฆ ยทe ๐ง) |
14 | 2 | cv 1541 |
. . . . 5
class ๐ฅ |
15 | 13, 14 | wceq 1542 |
. . . 4
wff (๐ฆ ยทe ๐ง) = ๐ฅ |
16 | 15, 10, 4 | crio 7316 |
. . 3
class
(โฉ๐ง
โ โ* (๐ฆ ยทe ๐ง) = ๐ฅ) |
17 | 2, 3, 4, 8, 16 | cmpo 7363 |
. 2
class (๐ฅ โ โ*,
๐ฆ โ (โ โ
{0}) โฆ (โฉ๐ง โ โ* (๐ฆ ยทe ๐ง) = ๐ฅ)) |
18 | 1, 17 | wceq 1542 |
1
wff
/๐ = (๐ฅ
โ โ*, ๐ฆ โ (โ โ {0}) โฆ
(โฉ๐ง โ
โ* (๐ฆ
ยทe ๐ง) =
๐ฅ)) |