Theorem neirr 2934

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

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

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 2701

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

This theorem is referenced by:  neldifsn  4746  frxp2  8084  poxp3  8090  frxp3  8091  ac5b  10391  0nnn  12182  1nuz2  12843  dprd2da  19941  dvlog  26576  legso  28562  hleqnid  28571  umgrnloop0  29072  usgrnloop0ALT  29168  nfrgr2v  30234  0ngrp  30473  neldifpr1  32495  neldifpr2  32496  assafld  33609  signswch  34528  signstfvneq0  34539  linedegen  36116  irrdiff  37299  prtlem400  38848  padd01  39790  padd02  39791  fiiuncl  45043  gpg5nbgrvtx03starlem1  48053  gpg5nbgrvtx03starlem2  48054  gpg5nbgrvtx03starlem3  48055  gpg5nbgrvtx13starlem1  48056  gpg5nbgrvtx13starlem2  48057  gpg5nbgrvtx13starlem3  48058  gpg5edgnedg  48115  rmsupp0  48353  lcoc0  48408