Theorem neirr 2941

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 2760	. 2 ⊢ 𝐴 = 𝐴
2		nne 2936	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 221	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1632   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933

This theorem is referenced by:  ssdifsnOLD  4464  neldifsn  4467  ac5b  9492  1nuz2  11957  dprd2da  18641  dvlog  24596  legso  25693  hleqnid  25702  umgrnloop0  26203  usgrnloop0ALT  26296  nfrgr2v  27426  0ngrp  27674  signswch  30947  signstfvneq0  30958  linedegen  32556  prtlem400  34659  padd01  35600  padd02  35601  fiiuncl  39733  rmsupp0  42659  lcoc0  42721