reu3

Description: A way to express restricted uniqueness. (Contributed by NM, 24-Oct-2006)

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

Proof

Step	Hyp	Ref	Expression
1		reurex	$⊢ \exists! x \in A φ \to \exists x \in A φ$
2		reu6	$⊢ \exists! x \in A φ \leftrightarrow \exists y \in A \forall x \in A (φ \leftrightarrow x = y)$
3		biimp	$⊢ (φ \leftrightarrow x = y) \to (φ \to x = y)$
4	3	ralimi	$⊢ \forall x \in A (φ \leftrightarrow x = y) \to \forall x \in A (φ \to x = y)$
5	4	reximi	$⊢ \exists y \in A \forall x \in A (φ \leftrightarrow x = y) \to \exists y \in A \forall x \in A (φ \to x = y)$
6	2 5	sylbi	$⊢ \exists! x \in A φ \to \exists y \in A \forall x \in A (φ \to x = y)$
7	1 6	jca	$⊢ \exists! x \in A φ \to (\exists x \in A φ \land \exists y \in A \forall x \in A (φ \to x = y))$
8		rexex	$⊢ \exists y \in A \forall x \in A (φ \to x = y) \to \exists y \forall x \in A (φ \to x = y)$
9	8	anim2i	$⊢ (\exists x \in A φ \land \exists y \in A \forall x \in A (φ \to x = y)) \to (\exists x \in A φ \land \exists y \forall x \in A (φ \to x = y))$
10		eu3v	$⊢ \exists! x (x \in A \land φ) \leftrightarrow (\exists x (x \in A \land φ) \land \exists y \forall x ((x \in A \land φ) \to x = y))$
11		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
12		df-rex	$⊢ \exists x \in A φ \leftrightarrow \exists x (x \in A \land φ)$
13		df-ral	$⊢ \forall x \in A (φ \to x = y) \leftrightarrow \forall x (x \in A \to (φ \to x = y))$
14		impexp	$⊢ ((x \in A \land φ) \to x = y) \leftrightarrow (x \in A \to (φ \to x = y))$
15	14	albii	$⊢ \forall x ((x \in A \land φ) \to x = y) \leftrightarrow \forall x (x \in A \to (φ \to x = y))$
16	13 15	bitr4i	$⊢ \forall x \in A (φ \to x = y) \leftrightarrow \forall x ((x \in A \land φ) \to x = y)$
17	16	exbii	$⊢ \exists y \forall x \in A (φ \to x = y) \leftrightarrow \exists y \forall x ((x \in A \land φ) \to x = y)$
18	12 17	anbi12i	$⊢ (\exists x \in A φ \land \exists y \forall x \in A (φ \to x = y)) \leftrightarrow (\exists x (x \in A \land φ) \land \exists y \forall x ((x \in A \land φ) \to x = y))$
19	10 11 18	3bitr4i	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \exists y \forall x \in A (φ \to x = y))$
20	9 19	sylibr	$⊢ (\exists x \in A φ \land \exists y \in A \forall x \in A (φ \to x = y)) \to \exists! x \in A φ$
21	7 20	impbii	$⊢ \exists! x \in A φ \leftrightarrow (\exists x \in A φ \land \exists y \in A \forall x \in A (φ \to x = y))$

Metamath Proof Explorer

Theorem reu3

Proof