HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem axreg 6720
Description: Axiom of Regularity expressed more compactly.
Assertion
Ref Expression
axreg
Distinct variable group:   ,,

Proof of Theorem axreg
StepHypRef Expression
1 ax-reg 6719 . 2
2119.23bi 1661 1
Colors of variables: wff set class
Syntax hints:   wn 3   wi 4   wa 357  wal 1445  wex 1450   wcel 1533
This theorem is referenced by:  zfregcl  6721  axregndlem2  7601
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-4 1605  ax-reg 6719
This theorem depends on definitions:  df-bi 175  df-ex 1451
Copyright terms: Public domain