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

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






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