# Metamath Proof Explorer

## Theorem rexdifsn

Description: Restricted existential quantification over a set with an element removed. (Contributed by NM, 4-Feb-2015)

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

### Proof

Step Hyp Ref Expression
1 eldifsn ${⊢}{x}\in \left({A}\setminus \left\{{B}\right\}\right)↔\left({x}\in {A}\wedge {x}\ne {B}\right)$
2 1 anbi1i ${⊢}\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)\wedge {\phi }\right)↔\left(\left({x}\in {A}\wedge {x}\ne {B}\right)\wedge {\phi }\right)$
3 anass ${⊢}\left(\left({x}\in {A}\wedge {x}\ne {B}\right)\wedge {\phi }\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {\phi }\right)\right)$
4 2 3 bitri ${⊢}\left({x}\in \left({A}\setminus \left\{{B}\right\}\right)\wedge {\phi }\right)↔\left({x}\in {A}\wedge \left({x}\ne {B}\wedge {\phi }\right)\right)$
5 4 rexbii2 ${⊢}\exists {x}\in \left({A}\setminus \left\{{B}\right\}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({x}\ne {B}\wedge {\phi }\right)$