Theorem reu6 2842

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

Assertion

Ref	Expression
reu6	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦))

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

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem reu6

Step	Hyp	Ref	Expression
1		df-reu 2397	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑))
2		19.28v 1854	. . . . 5 ⊢ (∀𝑥(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) ↔ (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))))
3		eleq1 2177	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
4		sbequ12 1727	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑))
5	3, 4	anbi12d 462	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑)))
6		equequ1 1671	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑦 ↔ 𝑦 = 𝑦))
7	5, 6	bibi12d 234	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ↔ ((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦)))
8		equid 1660	. . . . . . . . . . . 12 ⊢ 𝑦 = 𝑦
9	8	tbt 246	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ ((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦))
10		simpl 108	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) → 𝑦 ∈ 𝐴)
11	9, 10	sylbir 134	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝐴 ∧ [𝑦 / 𝑥]𝜑) ↔ 𝑦 = 𝑦) → 𝑦 ∈ 𝐴)
12	7, 11	syl6bi 162	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → 𝑦 ∈ 𝐴))
13	12	spimv 1765	. . . . . . . 8 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → 𝑦 ∈ 𝐴)
14		bi1 117	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))
15	14	expdimp 257	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝜑 → 𝑥 = 𝑦))
16		bi2 129	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ∧ 𝜑)))
17		simpr 109	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝜑)
18	16, 17	syl6 33	. . . . . . . . . . . 12 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
19	18	adantr 272	. . . . . . . . . . 11 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝑥 = 𝑦 → 𝜑))
20	15, 19	impbid 128	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ∧ 𝑥 ∈ 𝐴) → (𝜑 ↔ 𝑥 = 𝑦))
21	20	ex 114	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)))
22	21	sps 1500	. . . . . . . 8 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)))
23	13, 22	jca 302	. . . . . . 7 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))))
24	23	a5i 1505	. . . . . 6 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) → ∀𝑥(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))))
25		bi1 117	. . . . . . . . . . 11 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
26	25	imim2i 12	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)) → (𝑥 ∈ 𝐴 → (𝜑 → 𝑥 = 𝑦)))
27	26	impd 252	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))
28	27	adantl 273	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) → ((𝑥 ∈ 𝐴 ∧ 𝜑) → 𝑥 = 𝑦))
29		eleq1a 2186	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝐴 → (𝑥 = 𝑦 → 𝑥 ∈ 𝐴))
30	29	adantr 272	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) → (𝑥 = 𝑦 → 𝑥 ∈ 𝐴))
31	30	imp 123	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → 𝑥 ∈ 𝐴)
32		bi2 129	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
33	32	imim2i 12	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)) → (𝑥 ∈ 𝐴 → (𝑥 = 𝑦 → 𝜑)))
34	33	com23 78	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)) → (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝜑)))
35	34	imp 123	. . . . . . . . . . 11 ⊢ (((𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)) ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → 𝜑))
36	35	adantll 465	. . . . . . . . . 10 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 → 𝜑))
37	31, 36	jcai 307	. . . . . . . . 9 ⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) ∧ 𝑥 = 𝑦) → (𝑥 ∈ 𝐴 ∧ 𝜑))
38	37	ex 114	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) → (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ∧ 𝜑)))
39	28, 38	impbid 128	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦))
40	39	alimi 1414	. . . . . 6 ⊢ (∀𝑥(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))) → ∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦))
41	24, 40	impbii 125	. . . . 5 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))))
42		df-ral 2395	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦)))
43	42	anbi2i 450	. . . . 5 ⊢ ((𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)) ↔ (𝑦 ∈ 𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → (𝜑 ↔ 𝑥 = 𝑦))))
44	2, 41, 43	3bitr4i 211	. . . 4 ⊢ (∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ↔ (𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)))
45	44	exbii 1567	. . 3 ⊢ (∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)))
46		df-eu 1978	. . 3 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦∀𝑥((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ 𝑥 = 𝑦))
47		df-rex 2396	. . 3 ⊢ (∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦)))
48	45, 46, 47	3bitr4i 211	. 2 ⊢ (∃!𝑥(𝑥 ∈ 𝐴 ∧ 𝜑) ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦))
49	1, 48	bitri 183	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑦 ∈ 𝐴 ∀𝑥 ∈ 𝐴 (𝜑 ↔ 𝑥 = 𝑦))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104  ∀wal 1312  ∃wex 1451   ∈ wcel 1463  [wsb 1718  ∃!weu 1975  ∀wral 2390  ∃wrex 2391  ∃!wreu 2392

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-eu 1978  df-cleq 2108  df-clel 2111  df-ral 2395  df-rex 2396  df-reu 2397

This theorem is referenced by:  reu3  2843  reu6i  2844  reu8  2849  xpf1o  6691