# Metamath Proof Explorer

## Theorem mosub

Description: "At most one" remains true after substitution. (Contributed by NM, 9-Mar-1995)

Ref Expression
Hypothesis mosub.1 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion mosub ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {\phi }\right)$

### Proof

Step Hyp Ref Expression
1 mosub.1 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 moeq ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}={A}$
3 1 ax-gen ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 moexexvw ${⊢}\left({\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}={A}\wedge \forall {y}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\to {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {\phi }\right)$
5 2 3 4 mp2an ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}={A}\wedge {\phi }\right)$