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

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

Proof of Theorem neirr
StepHypRef Expression
1 eqid 2296 . 2  |-  A  =  A
2 nne 2463 . 2  |-  ( -.  A  =/=  A  <->  A  =  A )
31, 2mpbir 200 1  |-  -.  A  =/=  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1632    =/= wne 2459
This theorem is referenced by:  neldifsn  3764  cantnf  7411  ac5b  8121  1nuz2  10309  dprd2da  15293  dvlog  20014  0ngrp  20894  linedegen  24838  lineval3a  26186  sgplpte22  26241  isray2  26256  prtlem400  26841  padd01  30622  padd02  30623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator