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∖CDE↔A∈B∧A≠C∧A≠D∧A≠E

Proof

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