Theorem reu8 3690

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	cbvreuvw 3371	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
3		reu6 3683	. 2 ⊢ (∃!𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥))
4		dfbi2 474	. . . . 5 ⊢ ((𝜓 ↔ 𝑦 = 𝑥) ↔ ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
5	4	ralbii 3081	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
6		r19.26 3095	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
7		ancom 460	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑))
8		equcom 2020	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
9	8	imbi2i 336	. . . . . . . . 9 ⊢ ((𝜓 → 𝑥 = 𝑦) ↔ (𝜓 → 𝑦 = 𝑥))
10	9	ralbii 3081	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥))
11	10	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥)))
12		biimt 360	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ (𝑥 ∈ 𝐴 → 𝜑)))
13		df-ral 3051	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)))
14		bi2.04 387	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
15	14	albii 1821	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
16		eleq1w 2818	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
17	16, 1	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
18	17	bicomd 223	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
19	18	equcoms 2022	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
20	19	equsalvw 2006	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
21	13, 15, 20	3bitrri 298	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))
22	12, 21	bitrdi 287	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
23	11, 22	anbi12d 633	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
24	7, 23	bitrid 283	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
25	6, 24	bitr4id 290	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
26	5, 25	bitrid 283	. . 3 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
27	26	rexbiia 3080	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
28	2, 3, 27	3bitri 297	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540   ∈ wcel 2114  ∀wral 3050  ∃wrex 3059  ∃!wreu 3347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-10 2147  ax-12 2183

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clel 2810  df-ral 3051  df-rex 3060  df-reu 3350

This theorem is referenced by:  reu8nf  3826  updjud  9848  reusq0  15390  reumodprminv  16734  grpinveu  18906  addsq2reu  27409  2sqreulem1  27415  2sqreunnlem1  27418  grpoideu  30565  grpoinveu  30575  cvmlift3lem2  35493  euoreqb  47392  2reu8i  47396  2reuimp0  47397  paireqne  47794  pgnbgreunbgr  48408  itsclquadeu  49060