Theorem neirr

Description: No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015)

	Ref	Expression
Assertion	neirr	$$⊢\neg A\ne A$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2		nne	$$⊢\neg A\ne A\leftrightarrow A=A$$
3	1 2	mpbir	$$⊢\neg A\ne A$$