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 )