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

Theorem neirr 2609
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 2404 . 2  |-  A  =  A
2 nne 2606 . 2  |-  ( -.  A  =/=  A  <->  A  =  A )
31, 2mpbir 211 1  |-  -.  A  =/=  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1407    =/= wne 2600
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-cleq 2396  df-ne 2602
This theorem is referenced by:  neldifsn  4101  cantnfOLD  8168  ac5b  8892  1nuz2  11204  dprd2da  17413  dvlog  23328  legso  24371  hleqnid  24378  usgranloop0  24809  frgra2v  25428  0ngrp  25640  signswch  29037  signstfvneq0  29048  linedegen  30494  prtlem400  31906  padd01  32841  padd02  32842  rmsupp0  38485  lcoc0  38547
  Copyright terms: Public domain W3C validator