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

Theorem neirr 2787
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 2606 . 2 𝐴 = 𝐴
2 nne 2782 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 219 1 ¬ 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1474  wne 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599  df-ne 2778
This theorem is referenced by:  neldifsn  4258  ac5b  9157  1nuz2  11593  dprd2da  18207  dvlog  24111  legso  25209  hleqnid  25218  usgranloop0  25672  frgra2v  26289  0ngrp  26512  signswch  29767  signstfvneq0  29778  linedegen  31223  prtlem400  32973  padd01  33915  padd02  33916  fiiuncl  38059  umgrnloop0  40333  usgrnloop0ALT  40431  nfrgr2v  41441  rmsupp0  41942  lcoc0  42004
  Copyright terms: Public domain W3C validator