Re: [isabelle] A set is not its own member

The theorem that you request is already present and is called mem_not_refl. Similar proofs can be found in the file ZF/upair.thy.
Larry Paulson

On 16 Mar 2009, at 22:49, Victor Porton wrote:

A problem about Isabelle/ZF:

I have a set Z and need to construct a set which is not a member of Z.

I heard that with the axiom of foundation (see ZF.thy) it can be proved
that any set is not member of itself. (This solves the above stated

Could anyone guid me how I can prove that a set is not its own member in

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