Theorem eu6w 42236

Description: Replace ax-10 2129, ax-12 2166 in eu6 2562 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 1775	. . . . . . . 8 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
2		pm2.21 123	. . . . . . . . 9 ⊢ (¬ 𝜑 → (𝜑 → 𝑥 = 𝑦))
3	2	alimi 1805	. . . . . . . 8 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	1, 3	sylbir 234	. . . . . . 7 ⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
5		equequ2 2021	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑥 = 𝑧))
6	5	imbi2d 339	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜑 → 𝑥 = 𝑧)))
7	6	albidv 1915	. . . . . . . 8 ⊢ (𝑦 = 𝑧 → (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑥(𝜑 → 𝑥 = 𝑧)))
8	7	19.8aw 2045	. . . . . . 7 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
9	4, 8	syl 17	. . . . . 6 ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
10		biimp 214	. . . . . . . 8 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
11	10	alimi 1805	. . . . . . 7 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
12	11	eximi 1829	. . . . . 6 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
13	9, 12	ja 186	. . . . 5 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
14		eu6w.x	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝜑 ↔ 𝜓))
15		equequ1 2020	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑧 → (𝑥 = 𝑦 ↔ 𝑧 = 𝑦))
16	14, 15	imbi12d 343	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝜑 → 𝑥 = 𝑦) ↔ (𝜓 → 𝑧 = 𝑦)))
17	16	nfa1w 42235	. . . . . . . . . 10 ⊢ Ⅎ𝑥∀𝑥(𝜑 → 𝑥 = 𝑦)
18	14, 15	bibi12d 344	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → ((𝜑 ↔ 𝑥 = 𝑦) ↔ (𝜓 ↔ 𝑧 = 𝑦)))
19	18	nfa1w 42235	. . . . . . . . . 10 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
20	17, 19	nfim 1891	. . . . . . . . 9 ⊢ Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
21		19.38b 1835	. . . . . . . . . 10 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ((∃𝑥𝜑 → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ ∀𝑥(𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))))
22	16	cbvalvw 2031	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑦) ↔ ∀𝑧(𝜓 → 𝑧 = 𝑦))
23	18	cbvalvw 2031	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ ∀𝑧(𝜓 ↔ 𝑧 = 𝑦))
24	22, 23	imbi12i 349	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∀𝑧(𝜓 → 𝑧 = 𝑦) → ∀𝑧(𝜓 ↔ 𝑧 = 𝑦)))
25	24	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∀𝑧(𝜓 → 𝑧 = 𝑦) → ∀𝑧(𝜓 ↔ 𝑧 = 𝑦))))
26	25	spw 2029	. . . . . . . . . . . 12 ⊢ (∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
27	25	19.8aw 2045	. . . . . . . . . . . . 13 ⊢ ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
28		id 22	. . . . . . . . . . . . . 14 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
29	28	nfrd 1785	. . . . . . . . . . . . 13 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∃𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
30	27, 29	syl5 34	. . . . . . . . . . . 12 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ((∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
31	26, 30	impbid2 225	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
32	31	imbi2d 339	. . . . . . . . . 10 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ((∃𝑥𝜑 → ∀𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))))
33	21, 32	bitr3d 280	. . . . . . . . 9 ⊢ (Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → (∀𝑥(𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))))
34	20, 33	ax-mp 5	. . . . . . . 8 ⊢ (∀𝑥(𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
35	16	spw 2029	. . . . . . . . . . 11 ⊢ (∀𝑥(𝜑 → 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
36		id 22	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝜑)
37		eu6w.y	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜃))
38	37	ax12wlem 2120	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
39	38	com12 32	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
40	36, 39	embantd 59	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
41	35, 40	syl5 34	. . . . . . . . . 10 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
42	41	ancld 549	. . . . . . . . 9 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))))
43		albiim 1884	. . . . . . . . 9 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
44	42, 43	imbitrrdi 251	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
45	34, 44	mpgbi 1792	. . . . . . 7 ⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
46	45	eximdv 1912	. . . . . 6 ⊢ (∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
47	46	com12 32	. . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
48	13, 47	impbii 208	. . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
49	48	anbi2i 621	. . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
50		abai 825	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
51		eu3v 2558	. . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
52	49, 50, 51	3bitr4ri 303	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
53		abai 825	. . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
54		ancom 459	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑))
55		biimpr 219	. . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
56	55	alimi 1805	. . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
57	56	eximi 1829	. . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
58		exsbim 1997	. . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
59	57, 58	syl 17	. . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
60	59	biantru 528	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
61	53, 54, 60	3bitr4i 302	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
62	52, 61	bitri 274	1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394  ∀wal 1531  ∃wex 1773  Ⅎwnf 1777  ∃!weu 2556

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-ex 1774  df-nf 1778  df-mo 2528  df-eu 2557

This theorem is referenced by:  euabsn2w  42239