Metamath Proof Explorer

Theorem axreg2

Description: Axiom of Regularity expressed more compactly. (Contributed by NM, 14-Aug-2003)

Ref Expression
Assertion axreg2 
|- ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )

Proof

Step Hyp Ref Expression
1 ax-reg 
 |-  ( E. x x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )
2 1 19.23bi 
 |-  ( x e. y -> E. x ( x e. y /\ A. z ( z e. x -> -. z e. y ) ) )