Theorem mh-unprimbi 37374

Description: Shortest possible version of ax-un 7751 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 2151	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
2		elequ1 2151	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
3	2	imbi2d 343	. . . . . . 7 ⊢ (𝑣 = 𝑧 → ((𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
4	1, 3	imbi12d 347	. . . . . 6 ⊢ (𝑣 = 𝑧 → ((𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦))))
5		elequ2 2159	. . . . . . 7 ⊢ (𝑢 = 𝑤 → (𝑣 ∈ 𝑢 ↔ 𝑣 ∈ 𝑤))
6		elequ1 2151	. . . . . . . 8 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
7	6	imbi1d 344	. . . . . . 7 ⊢ (𝑢 = 𝑤 → ((𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦) ↔ (𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
8	5, 7	imbi12d 347	. . . . . 6 ⊢ (𝑢 = 𝑤 → ((𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
9	4, 8	alcomw 2077	. . . . 5 ⊢ (∀𝑣∀𝑢(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ ∀𝑢∀𝑣(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
10		impexp 456	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
11		elequ12 2162	. . . . . . . 8 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ∈ 𝑤 ↔ 𝑣 ∈ 𝑢))
12		elequ1 2151	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → (𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
13	12	adantl 487	. . . . . . . . 9 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
14		elequ1 2151	. . . . . . . . . 10 ⊢ (𝑧 = 𝑣 → (𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
15	14	adantr 486	. . . . . . . . 9 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
16	13, 15	imbi12d 347	. . . . . . . 8 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → ((𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
17	11, 16	imbi12d 347	. . . . . . 7 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
18	10, 17	bitrid 286	. . . . . 6 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
19	18	cbval2vw 2072	. . . . 5 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑣∀𝑢(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
20		bi2.04 392	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑤 ∈ 𝑧 → (𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦)))
21		elequ12 2162	. . . . . . . . 9 ⊢ ((𝑤 = 𝑣 ∧ 𝑧 = 𝑢) → (𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢))
22	21	ancoms 464	. . . . . . . 8 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢))
23		elequ1 2151	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
24	23	adantr 486	. . . . . . . . 9 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
25		elequ1 2151	. . . . . . . . . 10 ⊢ (𝑤 = 𝑣 → (𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
26	25	adantl 487	. . . . . . . . 9 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
27	24, 26	imbi12d 347	. . . . . . . 8 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
28	22, 27	imbi12d 347	. . . . . . 7 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑤 ∈ 𝑧 → (𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
29	20, 28	bitrid 286	. . . . . 6 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
30	29	cbval2vw 2072	. . . . 5 ⊢ (∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ∀𝑢∀𝑣(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
31	9, 19, 30	3bitr4i 306	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
32		19.23v 1974	. . . . 5 ⊢ (∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
33	32	albii 1851	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
34		19.21v 1971	. . . . 5 ⊢ (∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
35	34	albii 1851	. . . 4 ⊢ (∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
36	31, 33, 35	3bitr3i 304	. . 3 ⊢ (∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
37	36	exbii 1880	. 2 ⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
38		df-ex 1812	. 2 ⊢ (∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
39	37, 38	bitri 278	1 ⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1567  ∃wex 1811

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812

This theorem is used by: (None)