# Metamath Proof Explorer

## Theorem dfeu

Description: Rederive df-eu from the old definition eu6 . (Contributed by NM, 23-Mar-1995) (Proof shortened by Wolf Lammen, 25-May-2019) (Proof shortened by BJ, 7-Oct-2022) (Proof modification is discouraged.) Use df-eu instead. (New usage is discouraged.)

Ref Expression
Assertion dfeu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$

### Proof

Step Hyp Ref Expression
1 abai ${⊢}\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 \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
2 euex ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 2 pm4.71ri ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
4 moeu ${⊢}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 4 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 \left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\to \exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)\right)$
6 1 3 5 3bitr4i ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$