Theorem reu8 3703

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 3397	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃!𝑦 ∈ 𝐴 𝜓)
3		reu6 3696	. 2 ⊢ (∃!𝑦 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥))
4		dfbi2 479	. . . . 5 ⊢ ((𝜓 ↔ 𝑦 = 𝑥) ↔ ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
5	4	ralbii 3117	. . . 4 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)))
6		r19.26 3131	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
7		ancom 465	. . . . . 6 ⊢ ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑))
8		equcom 2045	. . . . . . . . . 10 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
9	8	imbi2i 339	. . . . . . . . 9 ⊢ ((𝜓 → 𝑥 = 𝑦) ↔ (𝜓 → 𝑦 = 𝑥))
10	9	ralbii 3117	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥))
11	10	a1i 11	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ↔ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥)))
12		biimt 363	. . . . . . . 8 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ (𝑥 ∈ 𝐴 → 𝜑)))
13		df-ral 3086	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)))
14		bi2.04 391	. . . . . . . . . 10 ⊢ ((𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
15	14	albii 1846	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 ∈ 𝐴 → (𝑦 = 𝑥 → 𝜓)) ↔ ∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)))
16		eleq1w 2852	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
17	16, 1	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑦 ∈ 𝐴 → 𝜓)))
18	17	bicomd 226	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
19	18	equcoms 2047	. . . . . . . . . 10 ⊢ (𝑦 = 𝑥 → ((𝑦 ∈ 𝐴 → 𝜓) ↔ (𝑥 ∈ 𝐴 → 𝜑)))
20	19	equsalvw 2031	. . . . . . . . 9 ⊢ (∀𝑦(𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜓)) ↔ (𝑥 ∈ 𝐴 → 𝜑))
21	13, 15, 20	3bitrri 301	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))
22	12, 21	bitrdi 290	. . . . . . 7 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓)))
23	11, 22	anbi12d 643	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 → ((∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦) ∧ 𝜑) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
24	7, 23	bitrid 286	. . . . 5 ⊢ (𝑥 ∈ 𝐴 → ((𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)) ↔ (∀𝑦 ∈ 𝐴 (𝜓 → 𝑦 = 𝑥) ∧ ∀𝑦 ∈ 𝐴 (𝑦 = 𝑥 → 𝜓))))
25	6, 24	bitr4id 293	. . . 4 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 ((𝜓 → 𝑦 = 𝑥) ∧ (𝑦 = 𝑥 → 𝜓)) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
26	5, 25	bitrid 286	. . 3 ⊢ (𝑥 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦))))
27	26	rexbiia 3116	. 2 ⊢ (∃𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝜓 ↔ 𝑦 = 𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))
28	2, 3, 27	3bitri 300	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝐴 (𝜑 ∧ ∀𝑦 ∈ 𝐴 (𝜓 → 𝑥 = 𝑦)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  ∃!wreu 3373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-10 2182  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clel 2844  df-ral 3086  df-rex 3096  df-reu 3376

This theorem is referenced by:  reu8nf  3837  updjud  9920  reusq0  15516  reumodprminv  16864  grpinveu  19041  addsq2reu  27570  2sqreulem1  27576  2sqreunnlem1  27579  grpoideu  30802  grpoinveu  30812  cvmlift3lem2  35745  euoreqb  47770  2reu8i  47774  2reuimp0  47775  paireqne  48184  pgnbgreunbgr  48814  itsclquadeu  49477