Theorem mh-unprimbi

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

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

Proof

Step	Hyp	Ref	Expression
1		elequ1	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ 𝑢 ↔ 𝑧 ∈ 𝑢 ) )
2		elequ1	⊢ ( 𝑣 = 𝑧 → ( 𝑣 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦 ) )
3	2	imbi2d	⊢ ( 𝑣 = 𝑧 → ( ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ↔ ( 𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) )
4	1 3	imbi12d	⊢ ( 𝑣 = 𝑧 → ( ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) ) )
5		elequ2	⊢ ( 𝑢 = 𝑤 → ( 𝑣 ∈ 𝑢 ↔ 𝑣 ∈ 𝑤 ) )
6		elequ1	⊢ ( 𝑢 = 𝑤 → ( 𝑢 ∈ 𝑥 ↔ 𝑤 ∈ 𝑥 ) )
7	6	imbi1d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ↔ ( 𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) )
8	5 7	imbi12d	⊢ ( 𝑢 = 𝑤 → ( ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ↔ ( 𝑣 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ) )
9	4 8	alcomw	⊢ ( ∀ 𝑣 ∀ 𝑢 ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ↔ ∀ 𝑢 ∀ 𝑣 ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) )
10		impexp	⊢ ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) )
11		elequ12	⊢ ( ( 𝑧 = 𝑣 ∧ 𝑤 = 𝑢 ) → ( 𝑧 ∈ 𝑤 ↔ 𝑣 ∈ 𝑢 ) )
12		elequ1	⊢ ( 𝑤 = 𝑢 → ( 𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥 ) )
13	12	adantl	⊢ ( ( 𝑧 = 𝑣 ∧ 𝑤 = 𝑢 ) → ( 𝑤 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥 ) )
14		elequ1	⊢ ( 𝑧 = 𝑣 → ( 𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦 ) )
15	14	adantr	⊢ ( ( 𝑧 = 𝑣 ∧ 𝑤 = 𝑢 ) → ( 𝑧 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦 ) )
16	13 15	imbi12d	⊢ ( ( 𝑧 = 𝑣 ∧ 𝑤 = 𝑢 ) → ( ( 𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) )
17	11 16	imbi12d	⊢ ( ( 𝑧 = 𝑣 ∧ 𝑤 = 𝑢 ) → ( ( 𝑧 ∈ 𝑤 → ( 𝑤 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ) ↔ ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ) )
18	10 17	bitrid	⊢ ( ( 𝑧 = 𝑣 ∧ 𝑤 = 𝑢 ) → ( ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ) )
19	18	cbval2vw	⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑣 ∀ 𝑢 ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) )
20		bi2.04	⊢ ( ( 𝑧 ∈ 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑤 ∈ 𝑧 → ( 𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦 ) ) )
21		elequ12	⊢ ( ( 𝑤 = 𝑣 ∧ 𝑧 = 𝑢 ) → ( 𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢 ) )
22	21	ancoms	⊢ ( ( 𝑧 = 𝑢 ∧ 𝑤 = 𝑣 ) → ( 𝑤 ∈ 𝑧 ↔ 𝑣 ∈ 𝑢 ) )
23		elequ1	⊢ ( 𝑧 = 𝑢 → ( 𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥 ) )
24	23	adantr	⊢ ( ( 𝑧 = 𝑢 ∧ 𝑤 = 𝑣 ) → ( 𝑧 ∈ 𝑥 ↔ 𝑢 ∈ 𝑥 ) )
25		elequ1	⊢ ( 𝑤 = 𝑣 → ( 𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦 ) )
26	25	adantl	⊢ ( ( 𝑧 = 𝑢 ∧ 𝑤 = 𝑣 ) → ( 𝑤 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦 ) )
27	24 26	imbi12d	⊢ ( ( 𝑧 = 𝑢 ∧ 𝑤 = 𝑣 ) → ( ( 𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦 ) ↔ ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) )
28	22 27	imbi12d	⊢ ( ( 𝑧 = 𝑢 ∧ 𝑤 = 𝑣 ) → ( ( 𝑤 ∈ 𝑧 → ( 𝑧 ∈ 𝑥 → 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ) )
29	20 28	bitrid	⊢ ( ( 𝑧 = 𝑢 ∧ 𝑤 = 𝑣 ) → ( ( 𝑧 ∈ 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) ) )
30	29	cbval2vw	⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝑧 ∈ 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ ∀ 𝑢 ∀ 𝑣 ( 𝑣 ∈ 𝑢 → ( 𝑢 ∈ 𝑥 → 𝑣 ∈ 𝑦 ) ) )
31	9 19 30	3bitr4i	⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ∀ 𝑤 ( 𝑧 ∈ 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
32		19.23v	⊢ ( ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
33	32	albii	⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) )
34		19.21v	⊢ ( ∀ 𝑤 ( 𝑧 ∈ 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
35	34	albii	⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝑧 ∈ 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
36	31 33 35	3bitr3i	⊢ ( ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
37	36	exbii	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
38		df-ex	⊢ ( ∃ 𝑦 ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) ↔ ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )
39	37 38	bitri	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥 ) → 𝑧 ∈ 𝑦 ) ↔ ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( 𝑧 ∈ 𝑥 → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑦 ) ) )