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 ) ) ) |
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 ) ) ) |