Metamath Proof Explorer

Theorem elriin

Description: Elementhood in a relative intersection. (Contributed by Mario Carneiro, 30-Dec-2016)

Ref Expression
Assertion elriin ( 𝐵 ∈ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 elin ⊢ ( 𝐵 ∈ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) ↔ ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ ∩ 𝑥 ∈ 𝑋 𝑆 ) )
2 eliin ⊢ ( 𝐵 ∈ 𝐴 → ( 𝐵 ∈ ∩ 𝑥 ∈ 𝑋 𝑆 ↔ ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 ) )
3 2 pm5.32i ⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐵 ∈ ∩ 𝑥 ∈ 𝑋 𝑆 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 ) )
4 1 3 bitri ⊢ ( 𝐵 ∈ ( 𝐴 ∩ ∩ 𝑥 ∈ 𝑋 𝑆 ) ↔ ( 𝐵 ∈ 𝐴 ∧ ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑆 ) )