# Metamath Proof Explorer

## Theorem rexdifi

Description: Restricted existential quantification over a difference. (Contributed by AV, 25-Oct-2023)

Ref Expression
Assertion rexdifi ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)\to \exists {x}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
2 df-ral ${⊢}\forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)$
3 nfa1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)$
4 simprl ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\wedge \left({x}\in {A}\wedge {\phi }\right)\right)\to {x}\in {A}$
5 con2 ${⊢}\left({x}\in {B}\to ¬{\phi }\right)\to \left({\phi }\to ¬{x}\in {B}\right)$
6 5 sps ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\to \left({\phi }\to ¬{x}\in {B}\right)$
7 6 com12 ${⊢}{\phi }\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\to ¬{x}\in {B}\right)$
8 7 adantl ${⊢}\left({x}\in {A}\wedge {\phi }\right)\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\to ¬{x}\in {B}\right)$
9 8 impcom ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\wedge \left({x}\in {A}\wedge {\phi }\right)\right)\to ¬{x}\in {B}$
10 4 9 eldifd ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\wedge \left({x}\in {A}\wedge {\phi }\right)\right)\to {x}\in \left({A}\setminus {B}\right)$
11 simprr ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\wedge \left({x}\in {A}\wedge {\phi }\right)\right)\to {\phi }$
12 10 11 jca ${⊢}\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\wedge \left({x}\in {A}\wedge {\phi }\right)\right)\to \left({x}\in \left({A}\setminus {B}\right)\wedge {\phi }\right)$
13 12 ex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\to \left(\left({x}\in {A}\wedge {\phi }\right)\to \left({x}\in \left({A}\setminus {B}\right)\wedge {\phi }\right)\right)$
14 3 13 eximd ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\to \left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\setminus {B}\right)\wedge {\phi }\right)\right)$
15 14 impcom ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to ¬{\phi }\right)\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\setminus {B}\right)\wedge {\phi }\right)$
16 1 2 15 syl2anb ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\setminus {B}\right)\wedge {\phi }\right)$
17 df-rex ${⊢}\exists {x}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\setminus {B}\right)\wedge {\phi }\right)$
18 16 17 sylibr ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {B}\phantom{\rule{.4em}{0ex}}¬{\phi }\right)\to \exists {x}\in \left({A}\setminus {B}\right)\phantom{\rule{.4em}{0ex}}{\phi }$