reu2

Description: A way to express restricted uniqueness. (Contributed by NM, 22-Nov-1994)

		Ref	Expression
	Assertion	reu2	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y))$

Proof

Step	Hyp	Ref	Expression
1		nfv	$⊢ Ⅎ y (x \in A \land φ)$
2	1	eu2	$⊢ \exists! x (x \in A \land φ) \leftrightarrow (\exists x (x \in A \land φ) \land \forall x \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y))$
3		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
4		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
5		df-ral	$⊢ \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y) \leftrightarrow \forall x (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
6		19.21v	$⊢ \forall y (x \in A \to (y \in A \to ((φ \land [y/ x] φ) \to x = y))) \leftrightarrow (x \in A \to \forall y (y \in A \to ((φ \land [y/ x] φ) \to x = y)))$
7		nfv	$⊢ Ⅎ x y \in A$
8		nfs1v	$⊢ Ⅎ x [y/ x] φ$
9	7 8	nfan	$⊢ Ⅎ x (y \in A \land [y/ x] φ)$
10		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
11		sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$
12	10 11	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ))$
13	9 12	sbiev	$⊢ [y/ x] (x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ)$
14	13	anbi2i	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((x \in A \land φ) \land (y \in A \land [y/ x] φ))$
15		an4	$⊢ ((x \in A \land φ) \land (y \in A \land [y/ x] φ)) \leftrightarrow ((x \in A \land y \in A) \land (φ \land [y/ x] φ))$
16	14 15	bitri	$⊢ ((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \leftrightarrow ((x \in A \land y \in A) \land (φ \land [y/ x] φ))$
17	16	imbi1i	$⊢ (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow (((x \in A \land y \in A) \land (φ \land [y/ x] φ)) \to x = y)$
18		impexp	$⊢ (((x \in A \land y \in A) \land (φ \land [y/ x] φ)) \to x = y) \leftrightarrow ((x \in A \land y \in A) \to ((φ \land [y/ x] φ) \to x = y))$
19		impexp	$⊢ ((x \in A \land y \in A) \to ((φ \land [y/ x] φ) \to x = y)) \leftrightarrow (x \in A \to (y \in A \to ((φ \land [y/ x] φ) \to x = y)))$
20	17 18 19	3bitri	$⊢ (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow (x \in A \to (y \in A \to ((φ \land [y/ x] φ) \to x = y)))$
21	20	albii	$⊢ \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow \forall y (x \in A \to (y \in A \to ((φ \land [y/ x] φ) \to x = y)))$
22		df-ral	$⊢ \forall y \in A ((φ \land [y/ x] φ) \to x = y) \leftrightarrow \forall y (y \in A \to ((φ \land [y/ x] φ) \to x = y))$
23	22	imbi2i	$⊢ (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y)) \leftrightarrow (x \in A \to \forall y (y \in A \to ((φ \land [y/ x] φ) \to x = y)))$
24	6 21 23	3bitr4i	$⊢ \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
25	24	albii	$⊢ \forall x \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y) \leftrightarrow \forall x (x \in A \to \forall y \in A ((φ \land [y/ x] φ) \to x = y))$
26	5 25	bitr4i	$⊢ \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y) \leftrightarrow \forall x \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y)$
27	4 26	anbi12i	$⊢ (\exists x \in A φ \land \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y)) \leftrightarrow (\exists x (x \in A \land φ) \land \forall x \forall y (((x \in A \land φ) \land [y/ x] (x \in A \land φ)) \to x = y))$
28	2 3 27	3bitr4i	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \forall x \in A \forall y \in A ((φ \land [y/ x] φ) \to x = y))$

Metamath Proof Explorer

Theorem reu2

Proof