Theorem axregszf

Description: Derivation of zfregs using ax-regs . (Contributed by BTernaryTau, 30-Dec-2025)

	Ref	Expression
Assertion	axregszf	$$⊢A\ne \varnothing \to \exists x\in Ax\cap A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2		axregscl	$$⊢\exists xx\in A\to \exists x\left(x\in A\wedge \forall y\left(y\in x\to \neg y\in A\right)\right)$$
3		disj1	$$⊢x\cap A=\varnothing \leftrightarrow \forall y\left(y\in x\to \neg y\in A\right)$$
4	3	rexbii	$$⊢\exists x\in Ax\cap A=\varnothing \leftrightarrow \exists x\in A\forall y\left(y\in x\to \neg y\in A\right)$$
5		df-rex	$$⊢\exists x\in A\forall y\left(y\in x\to \neg y\in A\right)\leftrightarrow \exists x\left(x\in A\wedge \forall y\left(y\in x\to \neg y\in A\right)\right)$$
6	4 5	bitr2i	$$⊢\exists x\left(x\in A\wedge \forall y\left(y\in x\to \neg y\in A\right)\right)\leftrightarrow \exists x\in Ax\cap A=\varnothing$$
7	2 6	sylib	$$⊢\exists xx\in A\to \exists x\in Ax\cap A=\varnothing$$
8	1 7	sylbi	$$⊢A\ne \varnothing \to \exists x\in Ax\cap A=\varnothing$$