Theorem neirr 2937

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  neldifsn  4744  frxp2  8074  poxp3  8080  frxp3  8081  ac5b  10366  0nnn  12158  1nuz2  12819  dprd2da  19954  dvlog  26585  legso  28575  hleqnid  28584  umgrnloop0  29085  usgrnloop0ALT  29181  nfrgr2v  30247  0ngrp  30486  neldifpr1  32508  neldifpr2  32509  assafld  33645  signswch  34569  signstfvneq0  34580  linedegen  36176  irrdiff  37359  prtlem400  38908  padd01  39849  padd02  39850  fiiuncl  45101  gpg5nbgrvtx03starlem1  48098  gpg5nbgrvtx03starlem2  48099  gpg5nbgrvtx03starlem3  48100  gpg5nbgrvtx13starlem1  48101  gpg5nbgrvtx13starlem2  48102  gpg5nbgrvtx13starlem3  48103  gpg5edgnedg  48160  rmsupp0  48398  lcoc0  48453