# Metamath Proof Explorer

## Theorem rexdifpr

Description: Restricted existential quantification over a set with two elements removed. (Contributed by Alexander van der Vekens, 7-Feb-2018)

Ref Expression
Assertion rexdifpr ${⊢}\exists {x}\in \left({A}\setminus \left\{{B},{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)$

### Proof

Step Hyp Ref Expression
1 eldifpr ${⊢}{x}\in \left({A}\setminus \left\{{B},{C}\right\}\right)↔\left({x}\in {A}\wedge {x}\ne {B}\wedge {x}\ne {C}\right)$
2 3anass ${⊢}\left({x}\in {A}\wedge {x}\ne {B}\wedge {x}\ne {C}\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\right)\right)$
3 1 2 bitri ${⊢}{x}\in \left({A}\setminus \left\{{B},{C}\right\}\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\right)\right)$
4 3 anbi1i ${⊢}\left({x}\in \left({A}\setminus \left\{{B},{C}\right\}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\right)\right)\wedge {\phi }\right)$
5 anass ${⊢}\left(\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\right)\right)\wedge {\phi }\right)↔\left({x}\in {A}\wedge \left(\left({x}\ne {B}\wedge {x}\ne {C}\right)\wedge {\phi }\right)\right)$
6 df-3an ${⊢}\left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)↔\left(\left({x}\ne {B}\wedge {x}\ne {C}\right)\wedge {\phi }\right)$
7 6 bicomi ${⊢}\left(\left({x}\ne {B}\wedge {x}\ne {C}\right)\wedge {\phi }\right)↔\left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)$
8 7 anbi2i ${⊢}\left({x}\in {A}\wedge \left(\left({x}\ne {B}\wedge {x}\ne {C}\right)\wedge {\phi }\right)\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)\right)$
9 5 8 bitri ${⊢}\left(\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\right)\right)\wedge {\phi }\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)\right)$
10 4 9 bitri ${⊢}\left({x}\in \left({A}\setminus \left\{{B},{C}\right\}\right)\wedge {\phi }\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)\right)$
11 10 rexbii2 ${⊢}\exists {x}\in \left({A}\setminus \left\{{B},{C}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\ne {B}\wedge {x}\ne {C}\wedge {\phi }\right)$