This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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