Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | eliin | |- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1w | |- ( y = w -> ( y e. C <-> w e. C ) ) |
|
2 | 1 | ralbidv | |- ( y = w -> ( A. x e. B y e. C <-> A. x e. B w e. C ) ) |
3 | eleq1 | |- ( w = A -> ( w e. C <-> A e. C ) ) |
|
4 | 3 | ralbidv | |- ( w = A -> ( A. x e. B w e. C <-> A. x e. B A e. C ) ) |
5 | df-iin | |- |^|_ x e. B C = { y | A. x e. B y e. C } |
|
6 | 2 4 5 | elab2gw | |- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) ) |