# Metamath Proof Explorer

## Theorem eldifpr

Description: Membership in a set with two elements removed. Similar to eldifsn and eldiftp . (Contributed by Mario Carneiro, 18-Jul-2017)

Ref Expression
Assertion eldifpr ${⊢}{A}\in \left({B}\setminus \left\{{C},{D}\right\}\right)↔\left({A}\in {B}\wedge {A}\ne {C}\wedge {A}\ne {D}\right)$

### Proof

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