Step | Hyp | Ref
| Expression |
1 | | celwise 35363 |
. 2
class
elwise |
2 | | vo |
. . 3
setvar π |
3 | | cvv 3441 |
. . 3
class
V |
4 | | vx |
. . . 4
setvar π₯ |
5 | | vy |
. . . 4
setvar π¦ |
6 | | vz |
. . . . . . . . 9
setvar π§ |
7 | 6 | cv 1539 |
. . . . . . . 8
class π§ |
8 | | vu |
. . . . . . . . . 10
setvar π’ |
9 | 8 | cv 1539 |
. . . . . . . . 9
class π’ |
10 | | vv |
. . . . . . . . . 10
setvar π£ |
11 | 10 | cv 1539 |
. . . . . . . . 9
class π£ |
12 | 2 | cv 1539 |
. . . . . . . . 9
class π |
13 | 9, 11, 12 | co 7337 |
. . . . . . . 8
class (π’ππ£) |
14 | 7, 13 | wceq 1540 |
. . . . . . 7
wff π§ = (π’ππ£) |
15 | 5 | cv 1539 |
. . . . . . 7
class π¦ |
16 | 14, 10, 15 | wrex 3070 |
. . . . . 6
wff
βπ£ β
π¦ π§ = (π’ππ£) |
17 | 4 | cv 1539 |
. . . . . 6
class π₯ |
18 | 16, 8, 17 | wrex 3070 |
. . . . 5
wff
βπ’ β
π₯ βπ£ β π¦ π§ = (π’ππ£) |
19 | 18, 6 | cab 2713 |
. . . 4
class {π§ β£ βπ’ β π₯ βπ£ β π¦ π§ = (π’ππ£)} |
20 | 4, 5, 3, 3, 19 | cmpo 7339 |
. . 3
class (π₯ β V, π¦ β V β¦ {π§ β£ βπ’ β π₯ βπ£ β π¦ π§ = (π’ππ£)}) |
21 | 2, 3, 20 | cmpt 5175 |
. 2
class (π β V β¦ (π₯ β V, π¦ β V β¦ {π§ β£ βπ’ β π₯ βπ£ β π¦ π§ = (π’ππ£)})) |
22 | 1, 21 | wceq 1540 |
1
wff elwise =
(π β V β¦ (π₯ β V, π¦ β V β¦ {π§ β£ βπ’ β π₯ βπ£ β π¦ π§ = (π’ππ£)})) |