Step | Hyp | Ref
| Expression |
1 | | cipf 21052 |
. 2
class
ยทif |
2 | | vg |
. . 3
setvar ๐ |
3 | | cvv 3447 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar ๐ฅ |
5 | | vy |
. . . 4
setvar ๐ฆ |
6 | 2 | cv 1541 |
. . . . 5
class ๐ |
7 | | cbs 17091 |
. . . . 5
class
Base |
8 | 6, 7 | cfv 6500 |
. . . 4
class
(Baseโ๐) |
9 | 4 | cv 1541 |
. . . . 5
class ๐ฅ |
10 | 5 | cv 1541 |
. . . . 5
class ๐ฆ |
11 | | cip 17146 |
. . . . . 6
class
ยท๐ |
12 | 6, 11 | cfv 6500 |
. . . . 5
class
(ยท๐โ๐) |
13 | 9, 10, 12 | co 7361 |
. . . 4
class (๐ฅ(ยท๐โ๐)๐ฆ) |
14 | 4, 5, 8, 8, 13 | cmpo 7363 |
. . 3
class (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ)) |
15 | 2, 3, 14 | cmpt 5192 |
. 2
class (๐ โ V โฆ (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |
16 | 1, 15 | wceq 1542 |
1
wff
ยทif = (๐ โ V โฆ (๐ฅ โ (Baseโ๐), ๐ฆ โ (Baseโ๐) โฆ (๐ฅ(ยท๐โ๐)๐ฆ))) |