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.
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and