Metamath Proof Explorer

Theorem elriin

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

Ref Expression
Assertion elriin ⊢ B ∈ A ∩ ⋂ x ∈ X S ↔ B ∈ A ∧ ∀ x ∈ X B ∈ S

Proof

Step Hyp Ref Expression
1 elin ⊢ B ∈ A ∩ ⋂ x ∈ X S ↔ B ∈ A ∧ B ∈ ⋂ x ∈ X S
2 eliin ⊢ B ∈ A → B ∈ ⋂ x ∈ X S ↔ ∀ x ∈ X B ∈ S
3 2 pm5.32i ⊢ B ∈ A ∧ B ∈ ⋂ x ∈ X S ↔ B ∈ A ∧ ∀ x ∈ X B ∈ S
4 1 3 bitri ⊢ B ∈ A ∩ ⋂ x ∈ X S ↔ B ∈ A ∧ ∀ x ∈ X B ∈ S