Theorem zfreg

Description: The Axiom of Regularity using abbreviations. Axiom 6 of TakeutiZaring p. 21. This is called the "weak form". Axiom Reg of BellMachover p. 480. There is also a "strong form", not requiring that A be a set, that can be proved with more difficulty (see zfregs ). (Contributed by NM, 26-Nov-1995) Replace sethood hypothesis with sethood antecedent. (Revised by BJ, 27-Apr-2021)

	Ref	Expression
Assertion	zfreg	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \exists x\in Ax\cap A=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		n0	$$⊢A\ne \varnothing \leftrightarrow \exists xx\in A$$
2	1	biimpi	$$⊢A\ne \varnothing \to \exists xx\in A$$
3	2	anim2i	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \left(A\in V\wedge \exists xx\in A\right)$$
4		zfregcl	$$⊢A\in V\to \left(\exists xx\in A\to \exists x\in A\forall y\in x\neg y\in A\right)$$
5	4	imp	$$⊢\left(A\in V\wedge \exists xx\in A\right)\to \exists x\in A\forall y\in x\neg y\in A$$
6		disj	$$⊢x\cap A=\varnothing \leftrightarrow \forall y\in x\neg y\in A$$
7	6	rexbii	$$⊢\exists x\in Ax\cap A=\varnothing \leftrightarrow \exists x\in A\forall y\in x\neg y\in A$$
8	7	biimpri	$$⊢\exists x\in A\forall y\in x\neg y\in A\to \exists x\in Ax\cap A=\varnothing$$
9	3 5 8	3syl	$$⊢\left(A\in V\wedge A\ne \varnothing \right)\to \exists x\in Ax\cap A=\varnothing$$