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	|- ( ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) <-> -. A. y -. A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )

Proof

Step	Hyp	Ref	Expression
1		elequ1	|- ( y = z -> ( y e. x <-> z e. x ) )
2	1	cbvexvw	|- ( E. y y e. x <-> E. z z e. x )
3		df-ex	|- ( E. z z e. x <-> -. A. z -. z e. x )
4	2 3	bitri	|- ( E. y y e. x <-> -. A. z -. z e. x )
5	4	imbi1i	|- ( ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) <-> ( -. A. z -. z e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) )
6		jarl	|- ( ( ( y e. x -> z e. y ) -> -. z e. x ) -> ( -. y e. x -> -. z e. x ) )
7	6	com12	|- ( -. y e. x -> ( ( ( y e. x -> z e. y ) -> -. z e. x ) -> -. z e. x ) )
8	7	alimdv	|- ( -. y e. x -> ( A. z ( ( y e. x -> z e. y ) -> -. z e. x ) -> A. z -. z e. x ) )
9	8	con3rr3	|- ( -. A. z -. z e. x -> ( -. y e. x -> -. A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) )
10	9	con4d	|- ( -. A. z -. z e. x -> ( A. z ( ( y e. x -> z e. y ) -> -. z e. x ) -> y e. x ) )
11	10	pm4.71rd	|- ( -. A. z -. z e. x -> ( A. z ( ( y e. x -> z e. y ) -> -. z e. x ) <-> ( y e. x /\ A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) ) )
12		pm5.5	|- ( y e. x -> ( ( y e. x -> z e. y ) <-> z e. y ) )
13	12	imbi1d	|- ( y e. x -> ( ( ( y e. x -> z e. y ) -> -. z e. x ) <-> ( z e. y -> -. z e. x ) ) )
14	13	albidv	|- ( y e. x -> ( A. z ( ( y e. x -> z e. y ) -> -. z e. x ) <-> A. z ( z e. y -> -. z e. x ) ) )
15	14	pm5.32i	|- ( ( y e. x /\ A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) <-> ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) )
16	11 15	bitr2di	|- ( -. A. z -. z e. x -> ( ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) <-> A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) )
17	16	exbidv	|- ( -. A. z -. z e. x -> ( E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) <-> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) )
18	17	pm5.74i	|- ( ( -. A. z -. z e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) <-> ( -. A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) )
19		ala1	|- ( A. z -. z e. x -> A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )
20	19	alrimiv	|- ( A. z -. z e. x -> A. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )
21	20	19.2d	|- ( A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )
22	21	biantrur	|- ( ( -. A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) <-> ( ( A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) /\ ( -. A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) ) )
23		pm4.83	|- ( ( ( A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) /\ ( -. A. z -. z e. x -> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) ) ) <-> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )
24	18 22 23	3bitri	|- ( ( -. A. z -. z e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) <-> E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )
25		df-ex	|- ( E. y A. z ( ( y e. x -> z e. y ) -> -. z e. x ) <-> -. A. y -. A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )
26	5 24 25	3bitri	|- ( ( E. y y e. x -> E. y ( y e. x /\ A. z ( z e. y -> -. z e. x ) ) ) <-> -. A. y -. A. z ( ( y e. x -> z e. y ) -> -. z e. x ) )