Step | Hyp | Ref
| Expression |
1 | | df-oprab 7416 |
. 2
β’
{β¨β¨π,
ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} = {π₯ β£ βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))} |
2 | | df-ot 4638 |
. . . . . . . . . 10
β’
β¨π, β, πβ© = β¨β¨π, ββ©, πβ© |
3 | 2 | eqeq2i 2744 |
. . . . . . . . 9
β’ (π₯ = β¨π, β, πβ© β π₯ = β¨β¨π, ββ©, πβ©) |
4 | 3 | biimpri 227 |
. . . . . . . 8
β’ (π₯ = β¨β¨π, ββ©, πβ© β π₯ = β¨π, β, πβ©) |
5 | 4 | eleq1d 2817 |
. . . . . . 7
β’ (π₯ = β¨β¨π, ββ©, πβ© β (π₯ β π β β¨π, β, πβ© β π)) |
6 | 5 | biimpar 477 |
. . . . . 6
β’ ((π₯ = β¨β¨π, ββ©, πβ© β§ β¨π, β, πβ© β π) β π₯ β π) |
7 | 6 | adantrr 714 |
. . . . 5
β’ ((π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ))) β π₯ β π) |
8 | 7 | exlimiv 1932 |
. . . 4
β’
(βπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ))) β π₯ β π) |
9 | 8 | exlimivv 1934 |
. . 3
β’
(βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ))) β π₯ β π) |
10 | 9 | abssi 4068 |
. 2
β’ {π₯ β£ βπβββπ(π₯ = β¨β¨π, ββ©, πβ© β§ (β¨π, β, πβ© β π β§ π β (ππΆβ)))} β π |
11 | 1, 10 | eqsstri 4017 |
1
β’
{β¨β¨π,
ββ©, πβ© β£ (β¨π, β, πβ© β π β§ π β (ππΆβ))} β π |