# Metamath Proof Explorer

## Theorem eu6

Description: Alternate definition of the unique existential quantifier df-eu not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993) This used to be the definition of the unique existential quantifier, while df-eu was then proved as dfeu . (Revised by BJ, 30-Sep-2022) (Proof shortened by Wolf Lammen, 3-Jan-2023) Remove use of ax-11 . (Revised by SN, 21-Sep-2023)

Ref Expression
Assertion eu6 ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$

### Proof

Step Hyp Ref Expression
1 dfmoeu ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)$
2 1 anbi2i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$
3 abai ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)\right)$
4 eu3v ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }\to {x}={y}\right)\right)$
5 2 3 4 3bitr4ri ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)$
6 abai ${⊢}\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\wedge \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
7 ancom ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\wedge \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
8 biimpr ${⊢}\left({\phi }↔{x}={y}\right)\to \left({x}={y}\to {\phi }\right)$
9 8 alimi ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
10 9 eximi ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)$
11 exsbim ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={y}\to {\phi }\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
12 10 11 syl ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
13 12 biantru ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)↔\left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\wedge \left(\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
14 6 7 13 3bitr4i ${⊢}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$
15 5 14 bitri ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {y}\phantom{\rule{.4em}{0ex}}\forall {x}\phantom{\rule{.4em}{0ex}}\left({\phi }↔{x}={y}\right)$