Step | Hyp | Ref
| Expression |
1 | | eleq2 2827 |
. . . . 5
β’ (π΄ = π΅ β ((π βΎt π’) β π΄ β (π βΎt π’) β π΅)) |
2 | 1 | rexbidv 3176 |
. . . 4
β’ (π΄ = π΅ β (βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅)) |
3 | 2 | 2ralbidv 3213 |
. . 3
β’ (π΄ = π΅ β (βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄ β βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅)) |
4 | 3 | rabbidv 3418 |
. 2
β’ (π΄ = π΅ β {π β Top β£ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} = {π β Top β£ βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅}) |
5 | | df-nlly 22834 |
. 2
β’
π-Locally π΄
= {π β Top β£
βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΄} |
6 | | df-nlly 22834 |
. 2
β’
π-Locally π΅
= {π β Top β£
βπ₯ β π βπ¦ β π₯ βπ’ β (((neiβπ)β{π¦}) β© π« π₯)(π βΎt π’) β π΅} |
7 | 4, 5, 6 | 3eqtr4g 2802 |
1
β’ (π΄ = π΅ β π-Locally π΄ = π-Locally π΅) |