Metamath Proof Explorer

Theorem eldifsn

Description: Membership in a set with an element removed. (Contributed by NM, 10-Oct-2007)

Ref Expression
Assertion eldifsn ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ A ≠ C

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ ¬ A ∈ C
2 elsng ⊢ A ∈ B → A ∈ C ↔ A = C
3 2 necon3bbid ⊢ A ∈ B → ¬ A ∈ C ↔ A ≠ C
4 3 pm5.32i ⊢ A ∈ B ∧ ¬ A ∈ C ↔ A ∈ B ∧ A ≠ C
5 1 4 bitri ⊢ A ∈ B ∖ C ↔ A ∈ B ∧ A ≠ C