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	⊢ ¬ 𝐴 ∈ 𝐴

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
2	1 1	eleq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑥 ↔ 𝐴 ∈ 𝐴 ) )
3	2	notbid	⊢ ( 𝑥 = 𝐴 → ( ¬ 𝑥 ∈ 𝑥 ↔ ¬ 𝐴 ∈ 𝐴 ) )
4		elirrv	⊢ ¬ 𝑥 ∈ 𝑥
5	3 4	vtoclg	⊢ ( 𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ 𝐴 )
6		pm2.01	⊢ ( ( 𝐴 ∈ 𝐴 → ¬ 𝐴 ∈ 𝐴 ) → ¬ 𝐴 ∈ 𝐴 )
7	5 6	ax-mp	⊢ ¬ 𝐴 ∈ 𝐴