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

Theorem neirr 2671
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 2467 . 2  |-  A  =  A
2 nne 2668 . 2  |-  ( -.  A  =/=  A  <->  A  =  A )
31, 2mpbir 209 1  |-  -.  A  =/=  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  neldifsn  4154  cantnfOLD  8130  ac5b  8854  1nuz2  11153  dprd2da  16878  dvlog  22757  legso  23709  usgranloop0  24053  frgra2v  24672  0ngrp  24886  signswch  28155  signstfvneq0  28166  linedegen  29367  prtlem400  30213  rmsupp0  32034  lcoc0  32096  padd01  34607  padd02  34608
  Copyright terms: Public domain W3C validator