Metamath Proof Explorer

Theorem eu2

Description: An alternate way of defining existential uniqueness. Definition 6.10 of TakeutiZaring p. 26. (Contributed by NM, 8-Jul-1994) (Proof shortened by Wolf Lammen, 2-Dec-2018)

Ref Expression
Hypothesis eu2.nf ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
Assertion eu2 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$

Proof

Step Hyp Ref Expression
1 eu2.nf ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 df-eu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
3 1 mo3 ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)$
4 3 anbi2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$
5 2 4 bitri ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({\phi }\wedge \left[{y}/{x}\right]{\phi }\right)\to {x}={y}\right)\right)$