Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  neirr Structured version   Visualization version   GIF version

Theorem neirr 2941
 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
StepHypRef Expression
1 eqid 2760 . 2 𝐴 = 𝐴
2 nne 2936 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 221 1 ¬ 𝐴𝐴
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1632   ≠ wne 2932 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933 This theorem is referenced by:  ssdifsnOLD  4464  neldifsn  4467  ac5b  9492  1nuz2  11957  dprd2da  18641  dvlog  24596  legso  25693  hleqnid  25702  umgrnloop0  26203  usgrnloop0ALT  26296  nfrgr2v  27426  0ngrp  27674  signswch  30947  signstfvneq0  30958  linedegen  32556  prtlem400  34659  padd01  35600  padd02  35601  fiiuncl  39733  rmsupp0  42659  lcoc0  42721
 Copyright terms: Public domain W3C validator