Step |
Hyp |
Ref |
Expression |
1 |
|
ineq1 |
|- ( z = B -> ( z i^i ~P ( x i^i y ) ) = ( B i^i ~P ( x i^i y ) ) ) |
2 |
1
|
unieqd |
|- ( z = B -> U. ( z i^i ~P ( x i^i y ) ) = U. ( B i^i ~P ( x i^i y ) ) ) |
3 |
2
|
sseq2d |
|- ( z = B -> ( ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) <-> ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) ) |
4 |
3
|
raleqbi1dv |
|- ( z = B -> ( A. y e. z ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) <-> A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) ) |
5 |
4
|
raleqbi1dv |
|- ( z = B -> ( A. x e. z A. y e. z ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) ) |
6 |
|
df-bases |
|- TopBases = { z | A. x e. z A. y e. z ( x i^i y ) C_ U. ( z i^i ~P ( x i^i y ) ) } |
7 |
5 6
|
elab2g |
|- ( B e. C -> ( B e. TopBases <-> A. x e. B A. y e. B ( x i^i y ) C_ U. ( B i^i ~P ( x i^i y ) ) ) ) |