[isabelle] More on foundation axiom

In ZF.thy the foundation axiom is:
  foundation:    "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"

Why there are no simplified version?
  foundation:    "A=0 | (\<exists>x\<in>A. x Int A=0)"
Isn't the latter more convenient in use?
So my question: Why there are no second version of foundation in Isabelle/ZF?
Victor Porton - http://portonvictor.org

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.