Theorem mh-regprimbi

Description: Shortest possible version of ax-reg in primitive symbols. The equivalence is nontrivial, but it still follows solely from the axioms of predicate calculus. (Contributed by Matthew House, 13-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		elequ1	⊢ ( 𝑦 = 𝑧 → ( 𝑦 ∈ 𝑥 ↔ 𝑧 ∈ 𝑥 ) )
2	1	cbvexvw	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑥 ↔ ∃ 𝑧 𝑧 ∈ 𝑥 )
3		df-ex	⊢ ( ∃ 𝑧 𝑧 ∈ 𝑥 ↔ ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 )
4	2 3	bitri	⊢ ( ∃ 𝑦 𝑦 ∈ 𝑥 ↔ ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 )
5	4	imbi1i	⊢ ( ( ∃ 𝑦 𝑦 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) ↔ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) )
6		jarl	⊢ ( ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) → ( ¬ 𝑦 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑥 ) )
7	6	com12	⊢ ( ¬ 𝑦 ∈ 𝑥 → ( ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) → ¬ 𝑧 ∈ 𝑥 ) )
8	7	alimdv	⊢ ( ¬ 𝑦 ∈ 𝑥 → ( ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) → ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 ) )
9	8	con3rr3	⊢ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ( ¬ 𝑦 ∈ 𝑥 → ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) )
10	9	con4d	⊢ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ( ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
11	10	pm4.71rd	⊢ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ( ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ) )
12		pm5.5	⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) ↔ 𝑧 ∈ 𝑦 ) )
13	12	imbi1d	⊢ ( 𝑦 ∈ 𝑥 → ( ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ↔ ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
14	13	albidv	⊢ ( 𝑦 ∈ 𝑥 → ( ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
15	14	pm5.32i	⊢ ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ↔ ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) )
16	11 15	bitr2di	⊢ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ( ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ↔ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) )
17	16	exbidv	⊢ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ( ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) )
18	17	pm5.74i	⊢ ( ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) ↔ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) )
19		ala1	⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )
20	19	alrimiv	⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∀ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )
21	20	19.2d	⊢ ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )
22	21	biantrur	⊢ ( ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ↔ ( ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ∧ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ) )
23		pm4.83	⊢ ( ( ( ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ∧ ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )
24	18 22 23	3bitri	⊢ ( ( ¬ ∀ 𝑧 ¬ 𝑧 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) ↔ ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )
25		df-ex	⊢ ( ∃ 𝑦 ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) ↔ ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )
26	5 24 25	3bitri	⊢ ( ( ∃ 𝑦 𝑦 ∈ 𝑥 → ∃ 𝑦 ( 𝑦 ∈ 𝑥 ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥 ) ) ) ↔ ¬ ∀ 𝑦 ¬ ∀ 𝑧 ( ( 𝑦 ∈ 𝑥 → 𝑧 ∈ 𝑦 ) → ¬ 𝑧 ∈ 𝑥 ) )