Theorem neirr 2787

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

Assertion

Ref	Expression
neirr	⊢ ¬ 𝐴 ≠ 𝐴

Proof of Theorem neirr

Step	Hyp	Ref	Expression
1		eqid 2606	. 2 ⊢ 𝐴 = 𝐴
2		nne 2782	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 219	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1474   ≠ wne 2776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-ext 2586

This theorem depends on definitions:  df-bi 195  df-cleq 2599  df-ne 2778

This theorem is referenced by:  neldifsn  4258  ac5b  9157  1nuz2  11593  dprd2da  18207  dvlog  24111  legso  25209  hleqnid  25218  usgranloop0  25672  frgra2v  26289  0ngrp  26512  signswch  29767  signstfvneq0  29778  linedegen  31223  prtlem400  32973  padd01  33915  padd02  33916  fiiuncl  38059  umgrnloop0  40333  usgrnloop0ALT  40431  nfrgr2v  41441  rmsupp0  41942  lcoc0  42004