# 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}\in \left({B}\setminus \left\{{C},{D},{E}\right\}\right)↔\left({A}\in {B}\wedge \left({A}\ne {C}\wedge {A}\ne {D}\wedge {A}\ne {E}\right)\right)$

### Proof

Step Hyp Ref Expression
1 eldif ${⊢}{A}\in \left({B}\setminus \left\{{C},{D},{E}\right\}\right)↔\left({A}\in {B}\wedge ¬{A}\in \left\{{C},{D},{E}\right\}\right)$
2 eltpg ${⊢}{A}\in {B}\to \left({A}\in \left\{{C},{D},{E}\right\}↔\left({A}={C}\vee {A}={D}\vee {A}={E}\right)\right)$
3 2 notbid ${⊢}{A}\in {B}\to \left(¬{A}\in \left\{{C},{D},{E}\right\}↔¬\left({A}={C}\vee {A}={D}\vee {A}={E}\right)\right)$
4 ne3anior ${⊢}\left({A}\ne {C}\wedge {A}\ne {D}\wedge {A}\ne {E}\right)↔¬\left({A}={C}\vee {A}={D}\vee {A}={E}\right)$
5 3 4 syl6bbr ${⊢}{A}\in {B}\to \left(¬{A}\in \left\{{C},{D},{E}\right\}↔\left({A}\ne {C}\wedge {A}\ne {D}\wedge {A}\ne {E}\right)\right)$
6 5 pm5.32i ${⊢}\left({A}\in {B}\wedge ¬{A}\in \left\{{C},{D},{E}\right\}\right)↔\left({A}\in {B}\wedge \left({A}\ne {C}\wedge {A}\ne {D}\wedge {A}\ne {E}\right)\right)$
7 1 6 bitri ${⊢}{A}\in \left({B}\setminus \left\{{C},{D},{E}\right\}\right)↔\left({A}\in {B}\wedge \left({A}\ne {C}\wedge {A}\ne {D}\wedge {A}\ne {E}\right)\right)$