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

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
StepHypRef Expression
1 eqid 2610 . 2 𝐴 = 𝐴
2 nne 2786 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 220 1 ¬ 𝐴𝐴
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator