eu1

Description: An alternate way to express uniqueness used by some authors. Exercise 2(b) of Margaris p. 110. (Contributed by NM, 20-Aug-1993) (Revised by Mario Carneiro, 7-Oct-2016) (Proof shortened by Wolf Lammen, 29-Oct-2018) Avoid ax-13 . (Revised by Wolf Lammen, 7-Feb-2023)

		Ref	Expression
	Hypothesis	eu1.nf	$⊢ Ⅎ y φ$
	Assertion	eu1	$⊢ \exists! x φ \leftrightarrow \exists x (φ \land \forall y ([y/ x] φ \to x = y))$

Proof

Step	Hyp	Ref	Expression
1		eu1.nf	$⊢ Ⅎ y φ$
2		nfs1v	$⊢ Ⅎ x [y/ x] φ$
3	2	euf	$⊢ \exists! y [y/ x] φ \leftrightarrow \exists x \forall y ([y/ x] φ \leftrightarrow y = x)$
4	1	sb8euv	$⊢ \exists! x φ \leftrightarrow \exists! y [y/ x] φ$
5	1	sb6rfv	$⊢ φ \leftrightarrow \forall y (y = x \to [y/ x] φ)$
6		equcom	$⊢ x = y \leftrightarrow y = x$
7	6	imbi2i	$⊢ ([y/ x] φ \to x = y) \leftrightarrow ([y/ x] φ \to y = x)$
8	7	albii	$⊢ \forall y ([y/ x] φ \to x = y) \leftrightarrow \forall y ([y/ x] φ \to y = x)$
9	5 8	anbi12ci	$⊢ (φ \land \forall y ([y/ x] φ \to x = y)) \leftrightarrow (\forall y ([y/ x] φ \to y = x) \land \forall y (y = x \to [y/ x] φ))$
10		albiim	$⊢ \forall y ([y/ x] φ \leftrightarrow y = x) \leftrightarrow (\forall y ([y/ x] φ \to y = x) \land \forall y (y = x \to [y/ x] φ))$
11	9 10	bitr4i	$⊢ (φ \land \forall y ([y/ x] φ \to x = y)) \leftrightarrow \forall y ([y/ x] φ \leftrightarrow y = x)$
12	11	exbii	$⊢ \exists x (φ \land \forall y ([y/ x] φ \to x = y)) \leftrightarrow \exists x \forall y ([y/ x] φ \leftrightarrow y = x)$
13	3 4 12	3bitr4i	$⊢ \exists! x φ \leftrightarrow \exists x (φ \land \forall y ([y/ x] φ \to x = y))$

Metamath Proof Explorer

Theorem eu1

Proof