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

Metamath Proof Explorer

Theorem elirr

Description: No class is a member of itself. Exercise 6 of TakeutiZaring p. 22. Theorem 1.9(i) of Schloeder p. 1. (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 (x \in x \leftrightarrow A \in A)$
3	2	notbid	$⊢ x = A \to (\neg x \in x \leftrightarrow \neg A \in A)$
4		elirrv	$⊢ \neg x \in x$
5	3 4	vtoclg	$⊢ A \in A \to \neg A \in A$
6		pm2.01	$⊢ (A \in A \to \neg A \in A) \to \neg A \in A$
7	5 6	ax-mp	$⊢ \neg A \in A$