Metamath Proof Explorer


Theorem eliind

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 )

Proof

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 )