pm14.12

		Ref	Expression
	Assertion	pm14.12	$⊢ \exists! x φ \to \forall x \forall y ((φ \land \underset{˙}{[} y / x \underset{˙}{]} φ) \to x = y)$

Step	Hyp	Ref	Expression
1		eumo	$⊢ \exists! x φ \to \exists^{*} x φ$
2		nfv	$⊢ Ⅎ y φ$
3	2	mo3	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land [y/ x] φ) \to x = y)$
4		sbsbc	$⊢ [y/ x] φ \leftrightarrow \underset{˙}{[} y / x \underset{˙}{]} φ$
5	4	anbi2i	$⊢ (φ \land [y/ x] φ) \leftrightarrow (φ \land \underset{˙}{[} y / x \underset{˙}{]} φ)$
6	5	imbi1i	$⊢ ((φ \land [y/ x] φ) \to x = y) \leftrightarrow ((φ \land \underset{˙}{[} y / x \underset{˙}{]} φ) \to x = y)$
7	6	2albii	$⊢ \forall x \forall y ((φ \land [y/ x] φ) \to x = y) \leftrightarrow \forall x \forall y ((φ \land \underset{˙}{[} y / x \underset{˙}{]} φ) \to x = y)$
8	3 7	bitri	$⊢ \exists^{*} x φ \leftrightarrow \forall x \forall y ((φ \land \underset{˙}{[} y / x \underset{˙}{]} φ) \to x = y)$
9	1 8	sylib	$⊢ \exists! x φ \to \forall x \forall y ((φ \land \underset{˙}{[} y / x \underset{˙}{]} φ) \to x = y)$

Metamath Proof Explorer