Theorem mh-prprimbi

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

	Ref	Expression
Assertion	mh-prprimbi	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)\leftrightarrow \neg \forall z\left(x\in z\to \neg y\in z\right)$$

Proof

Step	Hyp	Ref	Expression
1		jaob	$$⊢\left(\left(w=x\vee w=y\right)\to w\in z\right)\leftrightarrow \left(\left(w=x\to w\in z\right)\wedge \left(w=y\to w\in z\right)\right)$$
2	1	albii	$$⊢\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)\leftrightarrow \forall w\left(\left(w=x\to w\in z\right)\wedge \left(w=y\to w\in z\right)\right)$$
3		19.26	$$⊢\forall w\left(\left(w=x\to w\in z\right)\wedge \left(w=y\to w\in z\right)\right)\leftrightarrow \left(\forall w\left(w=x\to w\in z\right)\wedge \forall w\left(w=y\to w\in z\right)\right)$$
4		elequ1	$$⊢w=x\to \left(w\in z\leftrightarrow x\in z\right)$$
5	4	equsalvw	$$⊢\forall w\left(w=x\to w\in z\right)\leftrightarrow x\in z$$
6		elequ1	$$⊢w=y\to \left(w\in z\leftrightarrow y\in z\right)$$
7	6	equsalvw	$$⊢\forall w\left(w=y\to w\in z\right)\leftrightarrow y\in z$$
8	5 7	anbi12i	$$⊢\left(\forall w\left(w=x\to w\in z\right)\wedge \forall w\left(w=y\to w\in z\right)\right)\leftrightarrow \left(x\in z\wedge y\in z\right)$$
9	2 3 8	3bitri	$$⊢\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)\leftrightarrow \left(x\in z\wedge y\in z\right)$$
10	9	exbii	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)\leftrightarrow \exists z\left(x\in z\wedge y\in z\right)$$
11		exnalimn	$$⊢\exists z\left(x\in z\wedge y\in z\right)\leftrightarrow \neg \forall z\left(x\in z\to \neg y\in z\right)$$
12	10 11	bitri	$$⊢\exists z\forall w\left(\left(w=x\vee w=y\right)\to w\in z\right)\leftrightarrow \neg \forall z\left(x\in z\to \neg y\in z\right)$$