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	|- ( ( A e. V /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		n0	|- ( A =/= (/) <-> E. x x e. A )
2	1	biimpi	|- ( A =/= (/) -> E. x x e. A )
3	2	anim2i	|- ( ( A e. V /\ A =/= (/) ) -> ( A e. V /\ E. x x e. A ) )
4		zfregcl	|- ( A e. V -> ( E. x x e. A -> E. x e. A A. y e. x -. y e. A ) )
5	4	imp	|- ( ( A e. V /\ E. x x e. A ) -> E. x e. A A. y e. x -. y e. A )
6		disj	|- ( ( x i^i A ) = (/) <-> A. y e. x -. y e. A )
7	6	rexbii	|- ( E. x e. A ( x i^i A ) = (/) <-> E. x e. A A. y e. x -. y e. A )
8	7	biimpri	|- ( E. x e. A A. y e. x -. y e. A -> E. x e. A ( x i^i A ) = (/) )
9	3 5 8	3syl	|- ( ( A e. V /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )