Theorem reu8 3563

Description: Restricted uniqueness using implicit substitution. (Contributed by NM, 24-Oct-2006.)

Hypothesis

Ref	Expression
rmo4.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
reu8	⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

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

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem reu8

Step	Hyp	Ref	Expression
1		rmo4.1	. . 3 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
2	1	cbvreuv 3321	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
3		reu6 3556	. 2 ⊢ (∃!𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥))
4		dfbi2 466	. . . . 5 ⊢ ((𝜓 ↔ 𝑦 = 𝑥) ↔ ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
5	4	ralbii 3127	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
6		ancom 452	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑))
7		equcom 2115	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
8	7	imbi2i 327	. . . . . . . . 9 ⊢ ((𝜓 → 𝑥 = 𝑦) ↔ (𝜓 → 𝑦 = 𝑥))
9	8	ralbii 3127	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥))
10	9	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥)))
11		biimt 351	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ (𝑥 ∈ 𝐴 → 𝜑)))
12		df-ral 3060	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)))
13		bi2.04 377	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
14	13	albii 1914	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
15		eleq1w 2827	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
16	15, 1	imbi12d 335	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
17	16	bicomd 214	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
18	17	equcoms 2117	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
19	18	equsalvw 2101	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
20	12, 14, 19	3bitrri 289	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))
21	11, 20	syl6bb 278	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
22	10, 21	anbi12d 624	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
23	6, 22	syl5bb 274	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
24		r19.26 3211	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
25	23, 24	syl6rbbr 281	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
26	5, 25	syl5bb 274	. . 3 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
27	26	rexbiia 3187	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
28	2, 3, 27	3bitri 288	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384  ∀wal 1650   ∈ wcel 2155  ∀wral 3055  ∃wrex 3056  ∃!wreu 3057

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-cleq 2758  df-clel 2761  df-ral 3060  df-rex 3061  df-reu 3062

This theorem is referenced by:  reu8nf  3676  updjud  9015  reumodprminv  15802  grpinveu  17737  grpoideu  27841  grpoinveu  27851  cvmlift3lem2  31771