Step |
Hyp |
Ref |
Expression |
1 |
|
fveq2 |
|- ( j = J -> ( cls ` j ) = ( cls ` J ) ) |
2 |
1
|
fveq1d |
|- ( j = J -> ( ( cls ` j ) ` z ) = ( ( cls ` J ) ` z ) ) |
3 |
2
|
sseq1d |
|- ( j = J -> ( ( ( cls ` j ) ` z ) C_ x <-> ( ( cls ` J ) ` z ) C_ x ) ) |
4 |
3
|
anbi2d |
|- ( j = J -> ( ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) ) |
5 |
4
|
rexeqbi1dv |
|- ( j = J -> ( E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) ) |
6 |
5
|
ralbidv |
|- ( j = J -> ( A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) ) |
7 |
6
|
raleqbi1dv |
|- ( j = J -> ( A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) <-> A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) ) |
8 |
|
df-reg |
|- Reg = { j e. Top | A. x e. j A. y e. x E. z e. j ( y e. z /\ ( ( cls ` j ) ` z ) C_ x ) } |
9 |
7 8
|
elrab2 |
|- ( J e. Reg <-> ( J e. Top /\ A. x e. J A. y e. x E. z e. J ( y e. z /\ ( ( cls ` J ) ` z ) C_ x ) ) ) |