# Metamath Proof Explorer

## Theorem sbmo

Description: Substitution into an at-most-one quantifier. (Contributed by Jeff Madsen, 2-Sep-2009)

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

### Proof

Step Hyp Ref Expression
1 sbex ${⊢}\left[{y}/{x}\right]\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)$
2 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{z}={w}$
3 2 sblim ${⊢}\left[{y}/{x}\right]\left({\phi }\to {z}={w}\right)↔\left(\left[{y}/{x}\right]{\phi }\to {z}={w}\right)$
4 3 sbalv ${⊢}\left[{y}/{x}\right]\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {z}={w}\right)$
5 4 exbii ${⊢}\exists {w}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {z}={w}\right)$
6 1 5 bitri ${⊢}\left[{y}/{x}\right]\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)↔\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {z}={w}\right)$
7 df-mo ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)$
8 7 sbbii ${⊢}\left[{y}/{x}\right]{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }↔\left[{y}/{x}\right]\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {z}={w}\right)$
9 df-mo ${⊢}{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }↔\exists {w}\phantom{\rule{.4em}{0ex}}\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {z}={w}\right)$
10 6 8 9 3bitr4i ${⊢}\left[{y}/{x}\right]{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}{\phi }↔{\exists }^{*}{z}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$