Theorem 2eu5

Description: An alternate definition of double existential uniqueness (see 2eu4 ). A mistake sometimes made in the literature is to use E! x E! y to mean "exactly one x and exactly one y ". (For example, see Proposition 7.53 of TakeutiZaring p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining A. x E* y ph as an additional condition. The correct definition apparently has never been published. ( E* means "there exists at most one".) (Contributed by NM, 26-Oct-2003) Avoid ax-13 . (Revised by Wolf Lammen, 2-Oct-2023)

	Ref	Expression
Assertion	2eu5	$$⊢\left(\exists !x\exists !y\phi \wedge \forall x{\exists }^{*}y\phi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		2eu1v	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \leftrightarrow \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
2	1	pm5.32ri	$$⊢\left(\exists !x\exists !y\phi \wedge \forall x{\exists }^{*}y\phi \right)\leftrightarrow \left(\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\wedge \forall x{\exists }^{*}y\phi \right)$$
3		eumo	$$⊢\exists !y\exists x\phi \to {\exists }^{*}y\exists x\phi$$
4		2moexv	$$⊢{\exists }^{*}y\exists x\phi \to \forall x{\exists }^{*}y\phi$$
5	3 4	syl	$$⊢\exists !y\exists x\phi \to \forall x{\exists }^{*}y\phi$$
6	5	adantl	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \forall x{\exists }^{*}y\phi$$
7	6	pm4.71i	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\leftrightarrow \left(\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\wedge \forall x{\exists }^{*}y\phi \right)$$
8		2eu4	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\right)$$
9	2 7 8	3bitr2i	$$⊢\left(\exists !x\exists !y\phi \wedge \forall x{\exists }^{*}y\phi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\right)$$