Theorem neirr 2803

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

Step	Hyp	Ref	Expression
1		eqid 2622	. 2 |- A = A
2		nne 2798	. 2 |- ( -. A =/= A <-> A = A )
3	1, 2	mpbir 221	1 |- -. A =/= A

Syntax hints:   -. wn 3   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  ssdifsn  4318  neldifsn  4321  ac5b  9300  1nuz2  11764  dprd2da  18441  dvlog  24397  legso  25494  hleqnid  25503  umgrnloop0  26004  usgrnloop0ALT  26097  nfrgr2v  27136  0ngrp  27365  signswch  30638  signstfvneq0  30649  linedegen  32250  prtlem400  34155  padd01  35097  padd02  35098  fiiuncl  39234  rmsupp0  42149  lcoc0  42211