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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2728  df-ne 2933

This theorem is referenced by:  neldifsn  4691  ac5b  10057  0nnn  11831  1nuz2  12485  dprd2da  19383  dvlog  25493  legso  26644  hleqnid  26653  umgrnloop0  27154  usgrnloop0ALT  27247  nfrgr2v  28309  0ngrp  28546  neldifpr1  30554  neldifpr2  30555  signswch  32206  signstfvneq0  32217  frxp2  33471  poxp3  33476  frxp3  33477  linedegen  34131  irrdiff  35180  prtlem400  36570  padd01  37511  padd02  37512  fiiuncl  42227  rmsupp0  45320  lcoc0  45379