MPE Home 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