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

Theorem neirr 3022
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 2818 . 2 𝐴 = 𝐴
2 nne 3017 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 232 1 ¬ 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  neldifsn  4717  ac5b  9888  0nnn  11661  1nuz2  12312  dprd2da  19093  dvlog  25161  legso  26312  hleqnid  26321  umgrnloop0  26821  usgrnloop0ALT  26914  nfrgr2v  27978  0ngrp  28215  neldifpr1  30220  neldifpr2  30221  signswch  31730  signstfvneq0  31741  linedegen  33501  prtlem400  35886  padd01  36827  padd02  36828  fiiuncl  41204  rmsupp0  44344  lcoc0  44405
  Copyright terms: Public domain W3C validator