Metamath Proof Explorer


Theorem eliinid

Description: Membership in an indexed intersection implies membership in any intersected set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion eliinid ( ( 𝐴 𝑥𝐵 𝐶𝑥𝐵 ) → 𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 simpl ( ( 𝐴 𝑥𝐵 𝐶𝑥𝐵 ) → 𝐴 𝑥𝐵 𝐶 )
2 eliin ( 𝐴 𝑥𝐵 𝐶 → ( 𝐴 𝑥𝐵 𝐶 ↔ ∀ 𝑥𝐵 𝐴𝐶 ) )
3 2 adantr ( ( 𝐴 𝑥𝐵 𝐶𝑥𝐵 ) → ( 𝐴 𝑥𝐵 𝐶 ↔ ∀ 𝑥𝐵 𝐴𝐶 ) )
4 1 3 mpbid ( ( 𝐴 𝑥𝐵 𝐶𝑥𝐵 ) → ∀ 𝑥𝐵 𝐴𝐶 )
5 rspa ( ( ∀ 𝑥𝐵 𝐴𝐶𝑥𝐵 ) → 𝐴𝐶 )
6 4 5 sylancom ( ( 𝐴 𝑥𝐵 𝐶𝑥𝐵 ) → 𝐴𝐶 )