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

Theorem neirr 2832
 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 2651 . 2 𝐴 = 𝐴
2 nne 2827 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 221 1 ¬ 𝐴𝐴
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1523   ≠ wne 2823 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824 This theorem is referenced by:  ssdifsn  4351  neldifsn  4354  ac5b  9338  1nuz2  11802  dprd2da  18487  dvlog  24442  legso  25539  hleqnid  25548  umgrnloop0  26049  usgrnloop0ALT  26142  nfrgr2v  27252  0ngrp  27493  signswch  30766  signstfvneq0  30777  linedegen  32375  prtlem400  34474  padd01  35415  padd02  35416  fiiuncl  39548  rmsupp0  42474  lcoc0  42536
 Copyright terms: Public domain W3C validator