Metamath Proof Explorer

Theorem eldiftp

Description: Membership in a set with three elements removed. Similar to eldifsn and eldifpr . (Contributed by David A. Wheeler, 22-Jul-2017)

Ref Expression
Assertion eldiftp ⊢ A ∈ B ∖ C D E ↔ A ∈ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E

Proof

Step Hyp Ref Expression
1 eldif ⊢ A ∈ B ∖ C D E ↔ A ∈ B ∧ ¬ A ∈ C D E
2 eltpg ⊢ A ∈ B → A ∈ C D E ↔ A = C ∨ A = D ∨ A = E
3 2 notbid ⊢ A ∈ B → ¬ A ∈ C D E ↔ ¬ A = C ∨ A = D ∨ A = E
4 ne3anior ⊢ A ≠ C ∧ A ≠ D ∧ A ≠ E ↔ ¬ A = C ∨ A = D ∨ A = E
5 3 4 syl6bbr ⊢ A ∈ B → ¬ A ∈ C D E ↔ A ≠ C ∧ A ≠ D ∧ A ≠ E
6 5 pm5.32i ⊢ A ∈ B ∧ ¬ A ∈ C D E ↔ A ∈ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E
7 1 6 bitri ⊢ A ∈ B ∖ C D E ↔ A ∈ B ∧ A ≠ C ∧ A ≠ D ∧ A ≠ E