[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.