# Metamath Proof Explorer

## Theorem eu1

Description: An alternate way to express uniqueness used by some authors. Exercise 2(b) of Margaris p. 110. (Contributed by NM, 20-Aug-1993) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 29-Oct-2018) Avoid ax-13 . (Revised by Wolf Lammen, 7-Feb-2023)

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

### Proof

Step Hyp Ref Expression
1 eu1.nf ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfs1v ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
3 2 euf ${⊢}\exists !{y}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{y}={x}\right)$
4 1 sb8euv ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists !{y}\phantom{\rule{.4em}{0ex}}\left[{y}/{x}\right]{\phi }$
5 1 sb6rfv ${⊢}{\phi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left[{y}/{x}\right]{\phi }\right)$
6 equcom ${⊢}{x}={y}↔{y}={x}$
7 6 imbi2i ${⊢}\left(\left[{y}/{x}\right]{\phi }\to {x}={y}\right)↔\left(\left[{y}/{x}\right]{\phi }\to {y}={x}\right)$
8 7 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {x}={y}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {y}={x}\right)$
9 5 8 anbi12ci ${⊢}\left({\phi }\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {x}={y}\right)\right)↔\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {y}={x}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left[{y}/{x}\right]{\phi }\right)\right)$
10 albiim ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{y}={x}\right)↔\left(\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {y}={x}\right)\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left({y}={x}\to \left[{y}/{x}\right]{\phi }\right)\right)$
11 9 10 bitr4i ${⊢}\left({\phi }\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {x}={y}\right)\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{y}={x}\right)$
12 11 exbii ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {x}={y}\right)\right)↔\exists {x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }↔{y}={x}\right)$
13 3 4 12 3bitr4i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\wedge \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left[{y}/{x}\right]{\phi }\to {x}={y}\right)\right)$