Step | Hyp | Ref
| Expression |
1 | | ccf 9878 |
. 2
class
cf |
2 | | vx |
. . 3
setvar π₯ |
3 | | con0 6318 |
. . 3
class
On |
4 | | vy |
. . . . . . . . 9
setvar π¦ |
5 | 4 | cv 1541 |
. . . . . . . 8
class π¦ |
6 | | vz |
. . . . . . . . . 10
setvar π§ |
7 | 6 | cv 1541 |
. . . . . . . . 9
class π§ |
8 | | ccrd 9876 |
. . . . . . . . 9
class
card |
9 | 7, 8 | cfv 6497 |
. . . . . . . 8
class
(cardβπ§) |
10 | 5, 9 | wceq 1542 |
. . . . . . 7
wff π¦ = (cardβπ§) |
11 | 2 | cv 1541 |
. . . . . . . . 9
class π₯ |
12 | 7, 11 | wss 3911 |
. . . . . . . 8
wff π§ β π₯ |
13 | | vv |
. . . . . . . . . . . 12
setvar π£ |
14 | 13 | cv 1541 |
. . . . . . . . . . 11
class π£ |
15 | | vu |
. . . . . . . . . . . 12
setvar π’ |
16 | 15 | cv 1541 |
. . . . . . . . . . 11
class π’ |
17 | 14, 16 | wss 3911 |
. . . . . . . . . 10
wff π£ β π’ |
18 | 17, 15, 7 | wrex 3070 |
. . . . . . . . 9
wff
βπ’ β
π§ π£ β π’ |
19 | 18, 13, 11 | wral 3061 |
. . . . . . . 8
wff
βπ£ β
π₯ βπ’ β π§ π£ β π’ |
20 | 12, 19 | wa 397 |
. . . . . . 7
wff (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’) |
21 | 10, 20 | wa 397 |
. . . . . 6
wff (π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’)) |
22 | 21, 6 | wex 1782 |
. . . . 5
wff
βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’)) |
23 | 22, 4 | cab 2710 |
. . . 4
class {π¦ β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’))} |
24 | 23 | cint 4908 |
. . 3
class β© {π¦
β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’))} |
25 | 2, 3, 24 | cmpt 5189 |
. 2
class (π₯ β On β¦ β© {π¦
β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’))}) |
26 | 1, 25 | wceq 1542 |
1
wff cf = (π₯ β On β¦ β© {π¦
β£ βπ§(π¦ = (cardβπ§) β§ (π§ β π₯ β§ βπ£ β π₯ βπ’ β π§ π£ β π’))}) |