eu4

Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995)

		Ref	Expression
	Hypothesis	eu4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
	Assertion	eu4	$⊢ \exists! x φ \leftrightarrow (\exists x φ \land \forall x \forall y ((φ \land ψ) \to x = y))$

Step	Hyp	Ref	Expression
1		eu4.1	$⊢ x = y \to (φ \leftrightarrow ψ)$
2		df-eu	$⊢ \exists! x φ \leftrightarrow (\exists x φ \land \exists^{*} x φ)$
3	1	mo4	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land ψ) \to x = y)$
4	3	anbi2i	$⊢ (\exists x φ \land \exists^{*} x φ) \leftrightarrow (\exists x φ \land \forall x \forall y ((φ \land ψ) \to x = y))$
5	2 4	bitri	$⊢ \exists! x φ \leftrightarrow (\exists x φ \land \forall x \forall y ((φ \land ψ) \to x = y))$

Metamath Proof Explorer