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

Theorem neirr 2999
 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 2801 . 2 𝐴 = 𝐴
2 nne 2994 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 234 1 ¬ 𝐴𝐴
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1538   ≠ wne 2990 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-ne 2991 This theorem is referenced by:  neldifsn  4688  ac5b  9893  0nnn  11665  1nuz2  12316  dprd2da  19161  dvlog  25246  legso  26397  hleqnid  26406  umgrnloop0  26906  usgrnloop0ALT  26999  nfrgr2v  28061  0ngrp  28298  neldifpr1  30309  neldifpr2  30310  signswch  31945  signstfvneq0  31956  linedegen  33718  irrdiff  34741  prtlem400  36165  padd01  37106  padd02  37107  fiiuncl  41696  rmsupp0  44767  lcoc0  44828
 Copyright terms: Public domain W3C validator