Theorem neirr 2791

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 2610	. 2 ⊢ 𝐴 = 𝐴
2		nne 2786	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 220	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1475   ≠ wne 2780

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

This theorem depends on definitions:  df-bi 196  df-cleq 2603  df-ne 2782

This theorem is referenced by:  neldifsn  4262  ac5b  9183  1nuz2  11640  dprd2da  18264  dvlog  24197  legso  25294  hleqnid  25303  umgrnloop0  25775  usgranloop0  25909  frgra2v  26526  0ngrp  26749  signswch  29964  signstfvneq0  29975  linedegen  31420  prtlem400  33173  padd01  34115  padd02  34116  fiiuncl  38259  usgrnloop0ALT  40432  nfrgr2v  41442  rmsupp0  41943  lcoc0  42005  ssdifsn  42228