Metamath Proof Explorer

Theorem elinti

Description: Membership in class intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion elinti ⊢ A ∈ ⋂ B → C ∈ B → A ∈ C

Proof

Step Hyp Ref Expression
1 elintg ⊢ A ∈ ⋂ B → A ∈ ⋂ B ↔ ∀ x ∈ B A ∈ x
2 eleq2 ⊢ x = C → A ∈ x ↔ A ∈ C
3 2 rspccv ⊢ ∀ x ∈ B A ∈ x → C ∈ B → A ∈ C
4 1 3 biimtrdi ⊢ A ∈ ⋂ B → A ∈ ⋂ B → C ∈ B → A ∈ C
5 4 pm2.43i ⊢ A ∈ ⋂ B → C ∈ B → A ∈ C