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	$$⊢\forall x\in A\neg x\in x\to \neg A\in A$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢x=A\to \left(x\in x\leftrightarrow A\in x\right)$$
2		eleq2	$$⊢x=A\to \left(A\in x\leftrightarrow A\in A\right)$$
3	1 2	bitrd	$$⊢x=A\to \left(x\in x\leftrightarrow A\in A\right)$$
4	3	notbid	$$⊢x=A\to \left(\neg x\in x\leftrightarrow \neg A\in A\right)$$
5	4	rspccv	$$⊢\forall x\in A\neg x\in x\to \left(A\in A\to \neg A\in A\right)$$
6	5	pm2.01d	$$⊢\forall x\in A\neg x\in x\to \neg A\in A$$