Step | Hyp | Ref
| Expression |
1 | | cmp 10805 |
. 2
class
ยทP |
2 | | vx |
. . 3
setvar ๐ฅ |
3 | | vy |
. . 3
setvar ๐ฆ |
4 | | cnp 10802 |
. . 3
class
P |
5 | | vw |
. . . . . . . 8
setvar ๐ค |
6 | 5 | cv 1541 |
. . . . . . 7
class ๐ค |
7 | | vv |
. . . . . . . . 9
setvar ๐ฃ |
8 | 7 | cv 1541 |
. . . . . . . 8
class ๐ฃ |
9 | | vu |
. . . . . . . . 9
setvar ๐ข |
10 | 9 | cv 1541 |
. . . . . . . 8
class ๐ข |
11 | | cmq 10799 |
. . . . . . . 8
class
ยทQ |
12 | 8, 10, 11 | co 7362 |
. . . . . . 7
class (๐ฃ
ยทQ ๐ข) |
13 | 6, 12 | wceq 1542 |
. . . . . 6
wff ๐ค = (๐ฃ ยทQ ๐ข) |
14 | 3 | cv 1541 |
. . . . . 6
class ๐ฆ |
15 | 13, 9, 14 | wrex 3074 |
. . . . 5
wff
โ๐ข โ
๐ฆ ๐ค = (๐ฃ ยทQ ๐ข) |
16 | 2 | cv 1541 |
. . . . 5
class ๐ฅ |
17 | 15, 7, 16 | wrex 3074 |
. . . 4
wff
โ๐ฃ โ
๐ฅ โ๐ข โ ๐ฆ ๐ค = (๐ฃ ยทQ ๐ข) |
18 | 17, 5 | cab 2714 |
. . 3
class {๐ค โฃ โ๐ฃ โ ๐ฅ โ๐ข โ ๐ฆ ๐ค = (๐ฃ ยทQ ๐ข)} |
19 | 2, 3, 4, 4, 18 | cmpo 7364 |
. 2
class (๐ฅ โ P, ๐ฆ โ P โฆ
{๐ค โฃ โ๐ฃ โ ๐ฅ โ๐ข โ ๐ฆ ๐ค = (๐ฃ ยทQ ๐ข)}) |
20 | 1, 19 | wceq 1542 |
1
wff
ยทP = (๐ฅ โ P, ๐ฆ โ P โฆ {๐ค โฃ โ๐ฃ โ ๐ฅ โ๐ข โ ๐ฆ ๐ค = (๐ฃ ยทQ ๐ข)}) |