# Metamath Proof Explorer

## Theorem reu4

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 23-Nov-1994)

Ref Expression
Hypothesis rmo4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
Assertion reu4 ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$

### Proof

Step Hyp Ref Expression
1 rmo4.1 ${⊢}{x}={y}\to \left({\phi }↔{\psi }\right)$
2 reu5 ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\in {A}{\phi }\right)$
3 1 rmo4 ${⊢}{\exists }^{*}{x}\in {A}{\phi }↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)$
4 3 anbi2i ${⊢}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\in {A}{\phi }\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$
5 2 4 bitri ${⊢}\exists !{x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge {\psi }\right)\to {x}={y}\right)\right)$