Theorem neirr 2935

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 2730	. 2 ⊢ 𝐴 = 𝐴
2		nne 2930	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 231	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  neldifsn  4759  frxp2  8126  poxp3  8132  frxp3  8133  ac5b  10438  0nnn  12229  1nuz2  12890  dprd2da  19981  dvlog  26567  legso  28533  hleqnid  28542  umgrnloop0  29043  usgrnloop0ALT  29139  nfrgr2v  30208  0ngrp  30447  neldifpr1  32469  neldifpr2  32470  assafld  33640  signswch  34559  signstfvneq0  34570  linedegen  36138  irrdiff  37321  prtlem400  38870  padd01  39812  padd02  39813  fiiuncl  45066  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  rmsupp0  48360  lcoc0  48415