Theorem mh-unprimbi 36742

Description: Shortest possible version of ax-un 7682 in primitive symbols. (Contributed by Matthew House, 13-Apr-2026.)

Assertion

Ref	Expression
mh-unprimbi	⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))

Distinct variable groups:   𝑥,𝑤,𝑧   𝑦,𝑤,𝑧

Proof of Theorem mh-unprimbi

Dummy variables 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elequ1 2121	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
2		elequ1 2121	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
3	2	imbi2d 340	. . . . . . 7 ⊢ (𝑣 = 𝑧 → ((𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
4	1, 3	imbi12d 344	. . . . . 6 ⊢ (𝑣 = 𝑧 → ((𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦))))
5		elequ2 2129	. . . . . . 7 ⊢ (𝑢 = 𝑤 → (𝑣 ∈ 𝑢 ↔ 𝑣 ∈ 𝑤))
6		elequ1 2121	. . . . . . . 8 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
7	6	imbi1d 341	. . . . . . 7 ⊢ (𝑢 = 𝑤 → ((𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦) ↔ (𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
8	5, 7	imbi12d 344	. . . . . 6 ⊢ (𝑢 = 𝑤 → ((𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
9	4, 8	alcomw 2047	. . . . 5 ⊢ (∀𝑣∀𝑢(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ ∀𝑢∀𝑣(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
10		impexp 450	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
11		elequ12 2132	. . . . . . . 8 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ∈ 𝑤 ↔ 𝑣 ∈ 𝑢))
12		elequ1 2121	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → (𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
13	12	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
14		elequ1 2121	. . . . . . . . . 10 ⊢ (𝑧 = 𝑣 → (𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
15	14	adantr 480	. . . . . . . . 9 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
16	13, 15	imbi12d 344	. . . . . . . 8 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → ((𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
17	11, 16	imbi12d 344	. . . . . . 7 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
18	10, 17	bitrid 283	. . . . . 6 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
19	18	cbval2vw 2042	. . . . 5 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑣∀𝑢(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
20		bi2.04 387	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑤 ∈ 𝑧 → (𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦)))
21		elequ12 2132	. . . . . . . . 9 ⊢ ((𝑤 = 𝑣 ∧ 𝑧 = 𝑢) → (𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢))
22	21	ancoms 458	. . . . . . . 8 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢))
23		elequ1 2121	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
24	23	adantr 480	. . . . . . . . 9 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
25		elequ1 2121	. . . . . . . . . 10 ⊢ (𝑤 = 𝑣 → (𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
26	25	adantl 481	. . . . . . . . 9 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
27	24, 26	imbi12d 344	. . . . . . . 8 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
28	22, 27	imbi12d 344	. . . . . . 7 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑤 ∈ 𝑧 → (𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
29	20, 28	bitrid 283	. . . . . 6 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
30	29	cbval2vw 2042	. . . . 5 ⊢ (∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ∀𝑢∀𝑣(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
31	9, 19, 30	3bitr4i 303	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
32		19.23v 1944	. . . . 5 ⊢ (∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
33	32	albii 1821	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
34		19.21v 1941	. . . . 5 ⊢ (∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
35	34	albii 1821	. . . 4 ⊢ (∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
36	31, 33, 35	3bitr3i 301	. . 3 ⊢ (∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
37	36	exbii 1850	. 2 ⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
38		df-ex 1782	. 2 ⊢ (∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
39	37, 38	bitri 275	1 ⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395  ∀wal 1540  ∃wex 1781

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-9 2124

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782

This theorem is referenced by: (None)