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

Theorem neirr 2949
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 2737 . 2 𝐴 = 𝐴
2 nne 2944 . 2 𝐴𝐴𝐴 = 𝐴)
31, 2mpbir 231 1 ¬ 𝐴𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1540  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ne 2941
This theorem is referenced by:  neldifsn  4792  frxp2  8169  poxp3  8175  frxp3  8176  ac5b  10518  0nnn  12302  1nuz2  12966  dprd2da  20062  dvlog  26693  legso  28607  hleqnid  28616  umgrnloop0  29126  usgrnloop0ALT  29222  nfrgr2v  30291  0ngrp  30530  neldifpr1  32551  neldifpr2  32552  assafld  33688  signswch  34576  signstfvneq0  34587  linedegen  36144  irrdiff  37327  prtlem400  38871  padd01  39813  padd02  39814  fiiuncl  45070  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  rmsupp0  48284  lcoc0  48339
  Copyright terms: Public domain W3C validator