# Metamath Proof Explorer

## Theorem sbex

Description: Move existential quantifier in and out of substitution. (Contributed by NM, 27-Sep-2003)

Ref Expression
Assertion sbex ${⊢}\left[{z}/{y}\right]\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$

### Proof

Step Hyp Ref Expression
1 sbn ${⊢}\left[{z}/{y}\right]¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
2 sbn ${⊢}\left[{z}/{y}\right]¬{\phi }↔¬\left[{z}/{y}\right]{\phi }$
3 2 sbalv ${⊢}\left[{z}/{y}\right]\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}¬\left[{z}/{y}\right]{\phi }$
4 1 3 xchbinx ${⊢}\left[{z}/{y}\right]¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\left[{z}/{y}\right]{\phi }$
5 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
6 5 sbbii ${⊢}\left[{z}/{y}\right]\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left[{z}/{y}\right]¬\forall {x}\phantom{\rule{.4em}{0ex}}¬{\phi }$
7 df-ex ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}¬\left[{z}/{y}\right]{\phi }$
8 4 6 7 3bitr4i ${⊢}\left[{z}/{y}\right]\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left[{z}/{y}\right]{\phi }$