Metamath Proof Explorer


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 ) = (/) )