Metamath Proof Explorer


Theorem eliind

Description: Membership in indexed intersection. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses eliind.a ( 𝜑𝐴 𝑥𝐵 𝐶 )
eliind.k ( 𝜑𝐾𝐵 )
eliind.d ( 𝑥 = 𝐾 → ( 𝐴𝐶𝐴𝐷 ) )
Assertion eliind ( 𝜑𝐴𝐷 )

Proof

Step Hyp Ref Expression
1 eliind.a ( 𝜑𝐴 𝑥𝐵 𝐶 )
2 eliind.k ( 𝜑𝐾𝐵 )
3 eliind.d ( 𝑥 = 𝐾 → ( 𝐴𝐶𝐴𝐷 ) )
4 eliin ( 𝐴 𝑥𝐵 𝐶 → ( 𝐴 𝑥𝐵 𝐶 ↔ ∀ 𝑥𝐵 𝐴𝐶 ) )
5 1 4 syl ( 𝜑 → ( 𝐴 𝑥𝐵 𝐶 ↔ ∀ 𝑥𝐵 𝐴𝐶 ) )
6 1 5 mpbid ( 𝜑 → ∀ 𝑥𝐵 𝐴𝐶 )
7 3 6 2 rspcdva ( 𝜑𝐴𝐷 )