Metamath Proof Explorer

Theorem elin

Description: Expansion of membership in an intersection of two classes. Theorem 12 of Suppes p. 25. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion elin ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C

Proof

Step Hyp Ref Expression
1 elex ⊢ A ∈ B ∩ C → A ∈ V
2 elex ⊢ A ∈ C → A ∈ V
3 2 adantl ⊢ A ∈ B ∧ A ∈ C → A ∈ V
4 eleq1 ⊢ x = A → x ∈ B ↔ A ∈ B
5 eleq1 ⊢ x = A → x ∈ C ↔ A ∈ C
6 4 5 anbi12d ⊢ x = A → x ∈ B ∧ x ∈ C ↔ A ∈ B ∧ A ∈ C
7 df-in ⊢ B ∩ C = x | x ∈ B ∧ x ∈ C
8 6 7 elab2g ⊢ A ∈ V → A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C
9 1 3 8 pm5.21nii ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C