Theorem reu2 2914

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

Assertion

Ref	Expression
reu2	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))

Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reu2

Step	Hyp	Ref	Expression
1		nfv 1516	. . 3 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ∧ 𝜑)
2	1	eu2 2058	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦)))
3		df-reu 2451	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
4		df-rex 2450	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
5		df-ral 2449	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
6		19.21v 1861	. . . . . 6 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))))
7		nfv 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
8		nfs1v 1927	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥[𝑦 / 𝑥]𝜑
9	7, 8	nfan 1553	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)
10		eleq1 2229	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
11		sbequ12 1759	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
12	10, 11	anbi12d 465	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)))
13	9, 12	sbie 1779	. . . . . . . . . . 11 ⊢ ([𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑))
14	13	anbi2i 453	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)))
15		an4 576	. . . . . . . . . 10 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)))
16	14, 15	bitri 183	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)))
17	16	imbi1i 237	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦) ↔ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) → 𝑥 = 𝑦))
18		impexp 261	. . . . . . . 8 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝜑 ∧ [𝑦 / 𝑥]𝜑)) → 𝑥 = 𝑦) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
19		impexp 261	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))))
20	17, 18, 19	3bitri 205	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))))
21	20	albii 1458	. . . . . 6 ⊢ (∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))))
22		df-ral 2449	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑦(𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
23	22	imbi2i 225	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦))))
24	6, 21, 23	3bitr4i 211	. . . . 5 ⊢ (∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦) ↔ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
25	24	albii 1458	. . . 4 ⊢ (∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))
26	5, 25	bitr4i 186	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦) ↔ ∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦))
27	4, 26	anbi12i 456	. 2 ⊢ ((∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ∧ ∀𝑥∀𝑦(((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ [𝑦 / 𝑥](𝑥 ∈ 𝐴 ∧ 𝜑)) → 𝑥 = 𝑦)))
28	2, 3, 27	3bitr4i 211	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝜑 ∧ [𝑦 / 𝑥]𝜑) → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1341  ∃wex 1480  [wsb 1750  ∃!weu 2014   ∈ wcel 2136  ∀wral 2444  ∃wrex 2445  ∃!wreu 2446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-eu 2017  df-cleq 2158  df-clel 2161  df-ral 2449  df-rex 2450  df-reu 2451

This theorem is referenced by: (None)