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	$⊢ (\exists y y \in x \to \exists y (y \in x \land \forall z (z \in y \to \neg z \in x))) \leftrightarrow \neg \forall y \neg \forall z ((y \in x \to z \in y) \to \neg z \in x)$

Proof

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

Metamath Proof Explorer

Theorem mh-regprimbi

Proof