Theorem ac8prim

Description: ac8 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Assertion	ac8prim	$$⊢\left(\forall z\left(z\in x\to \exists ww\in z\right)\wedge \forall z\forall w\left(\left(z\in x\wedge w\in x\right)\to \left(\neg z=w\to \forall y\left(y\in z\to \neg y\in w\right)\right)\right)\right)\to \exists y\forall z\left(z\in x\to \exists w\forall v\left(\left(v\in z\wedge v\in y\right)\leftrightarrow v=w\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfac5prim	$$⊢\mathrm{CHOICE}\leftrightarrow \forall x\left(\left(\forall z\left(z\in x\to \exists ww\in z\right)\wedge \forall z\forall w\left(\left(z\in x\wedge w\in x\right)\to \left(\neg z=w\to \forall y\left(y\in z\to \neg y\in w\right)\right)\right)\right)\to \exists y\forall z\left(z\in x\to \exists w\forall v\left(\left(v\in z\wedge v\in y\right)\leftrightarrow v=w\right)\right)\right)$$
2	1	axaci	$$⊢\left(\forall z\left(z\in x\to \exists ww\in z\right)\wedge \forall z\forall w\left(\left(z\in x\wedge w\in x\right)\to \left(\neg z=w\to \forall y\left(y\in z\to \neg y\in w\right)\right)\right)\right)\to \exists y\forall z\left(z\in x\to \exists w\forall v\left(\left(v\in z\wedge v\in y\right)\leftrightarrow v=w\right)\right)$$