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 231	1 ⊢ ¬ 𝐴 ≠ 𝐴

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ne 2933

This theorem is referenced by:  neldifsn  4748  frxp2  8086  poxp3  8092  frxp3  8093  ac5b  10388  0nnn  12181  1nuz2  12837  dprd2da  19973  dvlog  26616  legso  28671  hleqnid  28680  umgrnloop0  29182  usgrnloop0ALT  29278  nfrgr2v  30347  0ngrp  30586  neldifpr1  32608  neldifpr2  32609  assafld  33794  signswch  34718  signstfvneq0  34729  linedegen  36337  irrdiff  37527  prtlem400  39126  padd01  40067  padd02  40068  fiiuncl  45306  gpg5nbgrvtx03starlem1  48310  gpg5nbgrvtx03starlem2  48311  gpg5nbgrvtx03starlem3  48312  gpg5nbgrvtx13starlem1  48313  gpg5nbgrvtx13starlem2  48314  gpg5nbgrvtx13starlem3  48315  gpg5edgnedg  48372  rmsupp0  48610  lcoc0  48664