Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class π΄ |
2 | 1 | wacn 9933 |
. 2
class AC
π΄ |
3 | | cvv 3475 |
. . . . 5
class
V |
4 | 1, 3 | wcel 2107 |
. . . 4
wff π΄ β V |
5 | | vy |
. . . . . . . . . 10
setvar π¦ |
6 | 5 | cv 1541 |
. . . . . . . . 9
class π¦ |
7 | | vg |
. . . . . . . . . 10
setvar π |
8 | 7 | cv 1541 |
. . . . . . . . 9
class π |
9 | 6, 8 | cfv 6544 |
. . . . . . . 8
class (πβπ¦) |
10 | | vf |
. . . . . . . . . 10
setvar π |
11 | 10 | cv 1541 |
. . . . . . . . 9
class π |
12 | 6, 11 | cfv 6544 |
. . . . . . . 8
class (πβπ¦) |
13 | 9, 12 | wcel 2107 |
. . . . . . 7
wff (πβπ¦) β (πβπ¦) |
14 | 13, 5, 1 | wral 3062 |
. . . . . 6
wff
βπ¦ β
π΄ (πβπ¦) β (πβπ¦) |
15 | 14, 7 | wex 1782 |
. . . . 5
wff
βπβπ¦ β π΄ (πβπ¦) β (πβπ¦) |
16 | | vx |
. . . . . . . . 9
setvar π₯ |
17 | 16 | cv 1541 |
. . . . . . . 8
class π₯ |
18 | 17 | cpw 4603 |
. . . . . . 7
class π«
π₯ |
19 | | c0 4323 |
. . . . . . . 8
class
β
|
20 | 19 | csn 4629 |
. . . . . . 7
class
{β
} |
21 | 18, 20 | cdif 3946 |
. . . . . 6
class
(π« π₯ β
{β
}) |
22 | | cmap 8820 |
. . . . . 6
class
βm |
23 | 21, 1, 22 | co 7409 |
. . . . 5
class
((π« π₯
β {β
}) βm π΄) |
24 | 15, 10, 23 | wral 3062 |
. . . 4
wff
βπ β
((π« π₯ β
{β
}) βm π΄)βπβπ¦ β π΄ (πβπ¦) β (πβπ¦) |
25 | 4, 24 | wa 397 |
. . 3
wff (π΄ β V β§ βπ β ((π« π₯ β {β
})
βm π΄)βπβπ¦ β π΄ (πβπ¦) β (πβπ¦)) |
26 | 25, 16 | cab 2710 |
. 2
class {π₯ β£ (π΄ β V β§ βπ β ((π« π₯ β {β
}) βm π΄)βπβπ¦ β π΄ (πβπ¦) β (πβπ¦))} |
27 | 2, 26 | wceq 1542 |
1
wff AC
π΄ = {π₯ β£ (π΄ β V β§ βπ β ((π« π₯ β {β
}) βm π΄)βπβπ¦ β π΄ (πβπ¦) β (πβπ¦))} |