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

Theorem neirr 2608
Description: No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)
Assertion
Ref Expression
neirr  |-  -.  A  =/=  A

Proof of Theorem neirr
StepHypRef Expression
1 eqid 2438 . 2  |-  A  =  A
2 nne 2607 . 2  |-  ( -.  A  =/=  A  <->  A  =  A )
31, 2mpbir 202 1  |-  -.  A  =/=  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1653    =/= wne 2601
This theorem is referenced by:  neldifsn  3931  cantnf  7651  ac5b  8360  1nuz2  10553  dprd2da  15602  dvlog  20544  usgranloop0  21402  0ngrp  21801  linedegen  26079  prtlem400  26721  cshwssizelem1a  28301  padd01  30670  padd02  30671
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-cleq 2431  df-ne 2603
  Copyright terms: Public domain W3C validator