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

Theorem neirr 2451
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 2283 . 2  |-  A  =  A
2 nne 2450 . 2  |-  ( -.  A  =/=  A  <->  A  =  A )
31, 2mpbir 200 1  |-  -.  A  =/=  A
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1623    =/= wne 2446
This theorem is referenced by:  neldifsn  3751  cantnf  7395  ac5b  8105  1nuz2  10293  dprd2da  15277  dvlog  19998  0ngrp  20878  linedegen  24766  lineval3a  26083  sgplpte22  26138  isray2  26153  prtlem400  26738  padd01  30000  padd02  30001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276  df-ne 2448
  Copyright terms: Public domain W3C validator