Theorem neirr 2978

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 2778	. 2 ⊢ 𝐴 = 𝐴
2		nne 2973	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 223	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1601   ≠ wne 2969

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-cleq 2770  df-ne 2970

This theorem is referenced by:  neldifsn  4554  ac5b  9635  0nnn  11411  1nuz2  12071  dprd2da  18828  dvlog  24834  legso  25950  hleqnid  25959  umgrnloop0  26457  usgrnloop0ALT  26551  nfrgr2v  27680  0ngrp  27938  signswch  31238  signstfvneq0  31250  linedegen  32839  prtlem400  35024  padd01  35965  padd02  35966  fiiuncl  40165  rmsupp0  43164  lcoc0  43226