Theorem reu8 3738

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 3403	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
3		reu6 3731	. 2 ⊢ (∃!𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥))
4		dfbi2 474	. . . . 5 ⊢ ((𝜓 ↔ 𝑦 = 𝑥) ↔ ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
5	4	ralbii 3092	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
6		r19.26 3110	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
7		ancom 460	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑))
8		equcom 2016	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
9	8	imbi2i 336	. . . . . . . . 9 ⊢ ((𝜓 → 𝑥 = 𝑦) ↔ (𝜓 → 𝑦 = 𝑥))
10	9	ralbii 3092	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥))
11	10	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥)))
12		biimt 360	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ (𝑥 ∈ 𝐴 → 𝜑)))
13		df-ral 3061	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)))
14		bi2.04 387	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
15	14	albii 1818	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
16		eleq1w 2823	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
17	16, 1	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
18	17	bicomd 223	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
19	18	equcoms 2018	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
20	19	equsalvw 2002	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
21	13, 15, 20	3bitrri 298	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))
22	12, 21	bitrdi 287	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
23	11, 22	anbi12d 632	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
24	7, 23	bitrid 283	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
25	6, 24	bitr4id 290	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
26	5, 25	bitrid 283	. . 3 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
27	26	rexbiia 3091	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
28	2, 3, 27	3bitri 297	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1537   ∈ wcel 2107  ∀wral 3060  ∃wrex 3069  ∃!wreu 3377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-10 2140  ax-12 2176

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clel 2815  df-ral 3061  df-rex 3070  df-reu 3380

This theorem is referenced by:  reu8nf  3876  updjud  9975  reusq0  15502  reumodprminv  16843  grpinveu  18993  addsq2reu  27485  2sqreulem1  27491  2sqreunnlem1  27494  grpoideu  30529  grpoinveu  30539  cvmlift3lem2  35326  euoreqb  47126  2reu8i  47130  2reuimp0  47131  paireqne  47503  itsclquadeu  48703