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

Theorem neirr 2613
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 2443 . 2  |-  A  =  A
2 nne 2612 . 2  |-  ( -.  A  =/=  A  <->  A  =  A )
31, 2mpbir 209 1  |-  -.  A  =/=  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1369    =/= wne 2606
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-cleq 2436  df-ne 2608
This theorem is referenced by:  neldifsn  4002  cantnfOLD  7923  ac5b  8647  1nuz2  10930  dprd2da  16541  dvlog  22096  usgranloop0  23299  0ngrp  23698  signswch  26962  signstfvneq0  26973  linedegen  28174  prtlem400  29015  frgra2v  30591  rmsupp0  30781  lcoc0  30956  padd01  33455  padd02  33456
  Copyright terms: Public domain W3C validator