Metamath Proof Explorer


Theorem zfregs

Description: The strong form of the Axiom of Regularity, which does not require that A be a set. Axiom 6' of TakeutiZaring p. 21. See also epfrs . (Contributed by NM, 17-Sep-2003)

Ref Expression
Assertion zfregs
|- ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )

Proof

Step Hyp Ref Expression
1 zfregfr
 |-  _E Fr A
2 epfrs
 |-  ( ( _E Fr A /\ A =/= (/) ) -> E. x e. A ( x i^i A ) = (/) )
3 1 2 mpan
 |-  ( A =/= (/) -> E. x e. A ( x i^i A ) = (/) )