Theorem neirr 2661

Description: No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.)

Assertion

Ref	Expression
neirr

Proof of Theorem neirr

Step	Hyp	Ref	Expression
1		eqid 2457	. 2
2		nne 2658	. 2
3	1, 2	mpbir 209	1

Syntax hints:  -.wn 3  =wceq 1395  =/=wne 2652

This theorem is referenced by:  neldifsn  4157  cantnfOLD  8155  ac5b  8879  1nuz2  11186  dprd2da  17091  dvlog  23032  legso  23985  hleqnid  23992  usgranloop0  24380  frgra2v  24999  0ngrp  25213  signswch  28518  signstfvneq0  28529  linedegen  29793  prtlem400  30611  rmsupp0  32961  lcoc0  33023  padd01  35535  padd02  35536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654