This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem untelirr

Description: We call a class "untanged" if all its members are not members of themselves. The term originates from Isbell (see citation in dfon2 ). Using this concept, we can avoid a lot of the uses of the Axiom of Regularity. Here, we prove a series of properties of untanged classes. First, we prove that an untangled class is not a member of itself. (Contributed by Scott Fenton, 28-Feb-2011)

		Ref	Expression
	Assertion	untelirr	\|- ( A. x e. A -. x e. x -> -. A e. A )

Proof

Step	Hyp	Ref	Expression
1		eleq1	\|- ( x = A -> ( x e. x <-> A e. x ) )
2		eleq2	\|- ( x = A -> ( A e. x <-> A e. A ) )
3	1 2	bitrd	\|- ( x = A -> ( x e. x <-> A e. A ) )
4	3	notbid	\|- ( x = A -> ( -. x e. x <-> -. A e. A ) )
5	4	rspccv	\|- ( A. x e. A -. x e. x -> ( A e. A -> -. A e. A ) )
6	5	pm2.01d	\|- ( A. x e. A -. x e. x -> -. A e. A )