Theorem mh-unprimbi 36785

Description: Shortest possible version of ax-un 7681 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 2128	. . . . . . 7 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢))
2		elequ1 2128	. . . . . . . 8 ⊢ (𝑣 = 𝑧 → (𝑣 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
3	2	imbi2d 342	. . . . . . 7 ⊢ (𝑣 = 𝑧 → ((𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
4	1, 3	imbi12d 346	. . . . . 6 ⊢ (𝑣 = 𝑧 → ((𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦))))
5		elequ2 2136	. . . . . . 7 ⊢ (𝑢 = 𝑤 → (𝑣 ∈ 𝑢 ↔ 𝑣 ∈ 𝑤))
6		elequ1 2128	. . . . . . . 8 ⊢ (𝑢 = 𝑤 → (𝑢 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥))
7	6	imbi1d 343	. . . . . . 7 ⊢ (𝑢 = 𝑤 → ((𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦) ↔ (𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
8	5, 7	imbi12d 346	. . . . . 6 ⊢ (𝑢 = 𝑤 → ((𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
9	4, 8	alcomw 2053	. . . . 5 ⊢ (∀𝑣∀𝑢(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)) ↔ ∀𝑢∀𝑣(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
10		impexp 452	. . . . . . 7 ⊢ (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦)))
11		elequ12 2139	. . . . . . . 8 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ∈ 𝑤 ↔ 𝑣 ∈ 𝑢))
12		elequ1 2128	. . . . . . . . . 10 ⊢ (𝑤 = 𝑢 → (𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
13	12	adantl 483	. . . . . . . . 9 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
14		elequ1 2128	. . . . . . . . . 10 ⊢ (𝑧 = 𝑣 → (𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
15	14	adantr 482	. . . . . . . . 9 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
16	13, 15	imbi12d 346	. . . . . . . 8 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → ((𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
17	11, 16	imbi12d 346	. . . . . . 7 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → ((𝑧 ∈ 𝑤 → (𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
18	10, 17	bitrid 285	. . . . . 6 ⊢ ((𝑧 = 𝑣 ∧ 𝑤 = 𝑢) → (((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
19	18	cbval2vw 2048	. . . . 5 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑣∀𝑢(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
20		bi2.04 389	. . . . . . 7 ⊢ ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑤 ∈ 𝑧 → (𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦)))
21		elequ12 2139	. . . . . . . . 9 ⊢ ((𝑤 = 𝑣 ∧ 𝑧 = 𝑢) → (𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢))
22	21	ancoms 460	. . . . . . . 8 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢))
23		elequ1 2128	. . . . . . . . . 10 ⊢ (𝑧 = 𝑢 → (𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
24	23	adantr 482	. . . . . . . . 9 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥))
25		elequ1 2128	. . . . . . . . . 10 ⊢ (𝑤 = 𝑣 → (𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
26	25	adantl 483	. . . . . . . . 9 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → (𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
27	24, 26	imbi12d 346	. . . . . . . 8 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦) ↔ (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
28	22, 27	imbi12d 346	. . . . . . 7 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑤 ∈ 𝑧 → (𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
29	20, 28	bitrid 285	. . . . . 6 ⊢ ((𝑧 = 𝑢 ∧ 𝑤 = 𝑣) → ((𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦))))
30	29	cbval2vw 2048	. . . . 5 ⊢ (∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ∀𝑢∀𝑣(𝑣 ∈ 𝑢 → (𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦)))
31	9, 19, 30	3bitr4i 305	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
32		19.23v 1950	. . . . 5 ⊢ (∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ (∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
33	32	albii 1827	. . . 4 ⊢ (∀𝑧∀𝑤((𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))
34		19.21v 1947	. . . . 5 ⊢ (∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ (𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
35	34	albii 1827	. . . 4 ⊢ (∀𝑧∀𝑤(𝑧 ∈ 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
36	31, 33, 35	3bitr3i 303	. . 3 ⊢ (∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
37	36	exbii 1856	. 2 ⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
38		df-ex 1788	. 2 ⊢ (∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))
39	37, 38	bitri 277	1 ⊢ (∃𝑦∀𝑧(∃𝑤(𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦) ↔ ¬ ∀𝑦 ¬ ∀𝑧(𝑧 ∈ 𝑥 → ∀𝑤(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 397  ∀wal 1546  ∃wex 1787

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131

This theorem depends on definitions:  df-bi 209  df-an 398  df-ex 1788

This theorem is referenced by: (None)