Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eliind.a | |- ( ph -> A e. |^|_ x e. B C ) |
|
eliind.k | |- ( ph -> K e. B ) |
||
eliind.d | |- ( x = K -> ( A e. C <-> A e. D ) ) |
||
Assertion | eliind | |- ( ph -> A e. D ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliind.a | |- ( ph -> A e. |^|_ x e. B C ) |
|
2 | eliind.k | |- ( ph -> K e. B ) |
|
3 | eliind.d | |- ( x = K -> ( A e. C <-> A e. D ) ) |
|
4 | eliin | |- ( A e. |^|_ x e. B C -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) ) |
|
5 | 1 4 | syl | |- ( ph -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) ) |
6 | 1 5 | mpbid | |- ( ph -> A. x e. B A e. C ) |
7 | 3 6 2 | rspcdva | |- ( ph -> A e. D ) |