dfmo

Description: Rederive df-mo from the old definition moeu . (Contributed by Wolf Lammen, 27-May-2019) (Proof modification is discouraged.) Use df-mo instead. (New usage is discouraged.)

		Ref	Expression
	Assertion	dfmo	$⊢ \exists^{*} x φ \leftrightarrow \exists y \forall x (φ \to x = y)$

Proof

Step	Hyp	Ref	Expression
1		moeu	$⊢ \exists^{*} x φ \leftrightarrow (\exists x φ \to \exists! x φ)$
2		eu6	$⊢ \exists! x φ \leftrightarrow \exists y \forall x (φ \leftrightarrow x = y)$
3	2	imbi2i	$⊢ (\exists x φ \to \exists! x φ) \leftrightarrow (\exists x φ \to \exists y \forall x (φ \leftrightarrow x = y))$
4		dfmoeu	$⊢ (\exists x φ \to \exists y \forall x (φ \leftrightarrow x = y)) \leftrightarrow \exists y \forall x (φ \to x = y)$
5	1 3 4	3bitri	$⊢ \exists^{*} x φ \leftrightarrow \exists y \forall x (φ \to x = y)$

Metamath Proof Explorer

Theorem dfmo

Proof