reu6

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

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

Proof

Step	Hyp	Ref	Expression
1		df-reu	$⊢ \exists! x \in A φ \leftrightarrow \exists! x (x \in A \land φ)$
2		19.28v	$⊢ \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \leftrightarrow (y \in A \land \forall x (x \in A \to (φ \leftrightarrow x = y)))$
3		eleq1w	$⊢ x = y \to (x \in A \leftrightarrow y \in A)$
4		sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$
5	3 4	anbi12d	$⊢ x = y \to ((x \in A \land φ) \leftrightarrow (y \in A \land [y/ x] φ))$
6		equequ1	$⊢ x = y \to (x = y \leftrightarrow y = y)$
7	5 6	bibi12d	$⊢ x = y \to (((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow ((y \in A \land [y/ x] φ) \leftrightarrow y = y))$
8		equid	$⊢ y = y$
9	8	tbt	$⊢ (y \in A \land [y/ x] φ) \leftrightarrow ((y \in A \land [y/ x] φ) \leftrightarrow y = y)$
10		simpl	$⊢ (y \in A \land [y/ x] φ) \to y \in A$
11	9 10	sylbir	$⊢ ((y \in A \land [y/ x] φ) \leftrightarrow y = y) \to y \in A$
12	7 11	biimtrdi	$⊢ x = y \to (((x \in A \land φ) \leftrightarrow x = y) \to y \in A)$
13	12	spimvw	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to y \in A$
14		ibar	$⊢ x \in A \to (φ \leftrightarrow (x \in A \land φ))$
15	14	bibi1d	$⊢ x \in A \to ((φ \leftrightarrow x = y) \leftrightarrow ((x \in A \land φ) \leftrightarrow x = y))$
16	15	biimprcd	$⊢ ((x \in A \land φ) \leftrightarrow x = y) \to (x \in A \to (φ \leftrightarrow x = y))$
17	16	sps	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to (x \in A \to (φ \leftrightarrow x = y))$
18	13 17	jca	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to (y \in A \land (x \in A \to (φ \leftrightarrow x = y)))$
19	18	axc4i	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \to \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y)))$
20		biimp	$⊢ (φ \leftrightarrow x = y) \to (φ \to x = y)$
21	20	imim2i	$⊢ (x \in A \to (φ \leftrightarrow x = y)) \to (x \in A \to (φ \to x = y))$
22	21	impd	$⊢ (x \in A \to (φ \leftrightarrow x = y)) \to ((x \in A \land φ) \to x = y)$
23	22	adantl	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to ((x \in A \land φ) \to x = y)$
24	3	biimprcd	$⊢ y \in A \to (x = y \to x \in A)$
25	24	adantr	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to (x = y \to x \in A)$
26	25	imp	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to x \in A$
27		simplr	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to (x \in A \to (φ \leftrightarrow x = y))$
28		simpr	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to x = y$
29		biimpr	$⊢ (φ \leftrightarrow x = y) \to (x = y \to φ)$
30	27 28 29	syl6ci	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to (x \in A \to φ)$
31	26 30	jcai	$⊢ ((y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \land x = y) \to (x \in A \land φ)$
32	31	ex	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to (x = y \to (x \in A \land φ))$
33	23 32	impbid	$⊢ (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to ((x \in A \land φ) \leftrightarrow x = y)$
34	33	alimi	$⊢ \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y))) \to \forall x ((x \in A \land φ) \leftrightarrow x = y)$
35	19 34	impbii	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow \forall x (y \in A \land (x \in A \to (φ \leftrightarrow x = y)))$
36		df-ral	$⊢ \forall x \in A (φ \leftrightarrow x = y) \leftrightarrow \forall x (x \in A \to (φ \leftrightarrow x = y))$
37	36	anbi2i	$⊢ (y \in A \land \forall x \in A (φ \leftrightarrow x = y)) \leftrightarrow (y \in A \land \forall x (x \in A \to (φ \leftrightarrow x = y)))$
38	2 35 37	3bitr4i	$⊢ \forall x ((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow (y \in A \land \forall x \in A (φ \leftrightarrow x = y))$
39	38	exbii	$⊢ \exists y \forall x ((x \in A \land φ) \leftrightarrow x = y) \leftrightarrow \exists y (y \in A \land \forall x \in A (φ \leftrightarrow x = y))$
40		eu6	$⊢ \exists! x (x \in A \land φ) \leftrightarrow \exists y \forall x ((x \in A \land φ) \leftrightarrow x = y)$
41		df-rex	$⊢ \exists y \in A \forall x \in A (φ \leftrightarrow x = y) \leftrightarrow \exists y (y \in A \land \forall x \in A (φ \leftrightarrow x = y))$
42	39 40 41	3bitr4i	$⊢ \exists! x (x \in A \land φ) \leftrightarrow \exists y \in A \forall x \in A (φ \leftrightarrow x = y)$
43	1 42	bitri	$⊢ \exists! x \in A φ \leftrightarrow \exists y \in A \forall x \in A (φ \leftrightarrow x = y)$

Metamath Proof Explorer

Theorem reu6

Proof