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 = y → x ∈ B ↔ y ∈ B
5 eleq1 ⊢ x = y → x ∈ C ↔ y ∈ C
6 4 5 anbi12d ⊢ x = y → x ∈ B ∧ x ∈ C ↔ y ∈ B ∧ y ∈ C
7 eleq1 ⊢ y = A → y ∈ B ↔ A ∈ B
8 eleq1 ⊢ y = A → y ∈ C ↔ A ∈ C
9 7 8 anbi12d ⊢ y = A → y ∈ B ∧ y ∈ C ↔ A ∈ B ∧ A ∈ C
10 df-in ⊢ B ∩ C = x | x ∈ B ∧ x ∈ C
11 6 9 10 elab2gw ⊢ A ∈ V → A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C
12 1 3 11 pm5.21nii ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C