Theorem eu6w 43687

Description: Replace ax-10 2178, ax-12 2213 in eu6 2600 with substitution hypotheses. (Contributed by SN, 27-May-2025.)

Hypotheses

Ref	Expression
eu6w.x	⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))
eu6w.y	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))

Assertion

Ref	Expression
eu6w	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦,𝑧   𝜓,𝑥   𝜃,𝑥   𝜑,𝑦,𝑧

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦, 𝑧)   𝜃(𝑦, 𝑧)

Proof of Theorem eu6w

Step	Hyp	Ref	Expression
1		alnex 1814	. . . . . . . 8 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		pm2.21 124	. . . . . . . . 9 ⊢ (¬ 𝜑 → (𝜑 → 𝑥 = 𝑦))
3	2	alimi 1844	. . . . . . . 8 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	1, 3	sylbir 238	. . . . . . 7 ⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
5		equequ2 2059	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
6	5	imbi2d 343	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜑 → 𝑥 = 𝑧)))
7	6	albidv 1953	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
8	7	19.8aw 2085	. . . . . . 7 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
9	4, 8	syl 18	. . . . . 6 ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
10		biimp 218	. . . . . . . 8 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
11	10	alimi 1844	. . . . . . 7 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
12	11	eximi 1868	. . . . . 6 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
13	9, 12	ja 188	. . . . 5 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
14		eu6w.x	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))
15		equequ1 2058	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
16	14, 15	imbi12d 347	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜓 → 𝑧 = 𝑦)))
17	16	nfa1w 43686	. . . . . . . . . 10 ⊢ Ⅎ𝑥∀𝑥(𝜑 → 𝑥 = 𝑦)
18	14, 15	bibi12d 348	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝜑 ↔ 𝑥 = 𝑦) ↔ (𝜓 ↔ 𝑧 = 𝑦)))
19	18	nfa1w 43686	. . . . . . . . . 10 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
20	17, 19	nfim 1929	. . . . . . . . 9 ⊢ Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
21		19.38b 1874	. . . . . . . . . 10 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ((∃𝑥𝜑 → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ ∀𝑥(𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))))
22	16	cbvalvw 2069	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑧(𝜓 → 𝑧 = 𝑦))
23	18	cbvalvw 2069	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∀𝑧(𝜓 ↔ 𝑧 = 𝑦))
24	22, 23	imbi12i 353	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∀𝑧(𝜓 → 𝑧 = 𝑦) → ∀𝑧(𝜓 ↔ 𝑧 = 𝑦)))
25	24	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∀𝑧(𝜓 → 𝑧 = 𝑦) → ∀𝑧(𝜓 ↔ 𝑧 = 𝑦))))
26	25	spw 2067	. . . . . . . . . . . 12 ⊢ (∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
27	25	19.8aw 2085	. . . . . . . . . . . . 13 ⊢ ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
28		id 23	. . . . . . . . . . . . . 14 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
29	28	nfrd 1824	. . . . . . . . . . . . 13 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∃𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
30	27, 29	syl5 35	. . . . . . . . . . . 12 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
31	26, 30	impbid2 229	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
32	31	imbi2d 343	. . . . . . . . . 10 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ((∃𝑥𝜑 → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))))
33	21, 32	bitr3d 284	. . . . . . . . 9 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∀𝑥(𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))))
34	20, 33	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑥(𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
35	16	spw 2067	. . . . . . . . . . 11 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
36		id 23	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝜑)
37		eu6w.y	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))
38	37	ax12wlem 2169	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
39	38	com12 33	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
40	36, 39	embantd 60	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
41	35, 40	syl5 35	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
42	41	ancld 560	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))))
43		albiim 1922	. . . . . . . . 9 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
44	42, 43	imbitrrdi 255	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
45	34, 44	mpgbi 1831	. . . . . . 7 ⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
46	45	eximdv 1950	. . . . . 6 ⊢ (∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
47	46	com12 33	. . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
48	13, 47	impbii 212	. . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
49	48	anbi2i 635	. . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
50		abai 839	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
51		eu3v 2596	. . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
52	49, 50, 51	3bitr4ri 307	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
53		abai 839	. . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
54		ancom 466	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑))
55		biimpr 223	. . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
56	55	alimi 1844	. . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
57	56	eximi 1868	. . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
58		exsbim 2035	. . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
59	57, 58	syl 18	. . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
60	59	biantru 539	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
61	53, 54, 60	3bitr4i 306	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
62	52, 61	bitri 278	1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  Ⅎwnf 1816  ∃!weu 2594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-mo 2565  df-eu 2595

This theorem is used by:  euabsn2w  43690