Metamath Proof Explorer

Theorem elinlem

Description: Two ways to say a set is a member of an intersection. (Contributed by RP, 19-Aug-2020)

Ref Expression
Assertion elinlem ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ I ⁡ A ∈ C

Proof

Step Hyp Ref Expression
1 elin ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ A ∈ C
2 fvi ⊢ A ∈ B → I ⁡ A = A
3 2 eqcomd ⊢ A ∈ B → A = I ⁡ A
4 3 eleq1d ⊢ A ∈ B → A ∈ C ↔ I ⁡ A ∈ C
5 4 pm5.32i ⊢ A ∈ B ∧ A ∈ C ↔ A ∈ B ∧ I ⁡ A ∈ C
6 1 5 bitri ⊢ A ∈ B ∩ C ↔ A ∈ B ∧ I ⁡ A ∈ C