Theorem elirr

Description: No class is a member of itself. Exercise 6 of TakeutiZaring p. 22. (Contributed by NM, 7-Aug-1994) (Proof shortened by Andrew Salmon, 9-Jul-2011)

	Ref	Expression
Assertion	elirr	$$⊢\neg A\in A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢x=A\to x=A$$
2	1 1	eleq12d	$$⊢x=A\to \left(x\in x\leftrightarrow A\in A\right)$$
3	2	notbid	$$⊢x=A\to \left(\neg x\in x\leftrightarrow \neg A\in A\right)$$
4		elirrv	$$⊢\neg x\in x$$
5	3 4	vtoclg	$$⊢A\in A\to \neg A\in A$$
6		pm2.01	$$⊢\left(A\in A\to \neg A\in A\right)\to \neg A\in A$$
7	5 6	ax-mp	$$⊢\neg A\in A$$