Theorem neirr 2965

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 2761	. 2 ⊢ 𝐴 = 𝐴
2		nne 2960	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 233	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  pssirr  4056  neldifsn  4751  frxp2  8119  poxp3  8125  frxp3  8126  ac5b  10432  0nnn  12246  1nuz2  12922  dprd2da  20067  dvlog  26693  legso  28745  hleqnid  28754  umgrnloop0  29256  usgrnloop0ALT  29352  nfrgr2v  30420  0ngrp  30660  neldifpr1  32681  neldifpr2  32682  assafld  33895  signswch  34819  signstfvneq0  34830  linedegen  36457  irrdiff  37782  prtlem400  39458  padd01  40399  padd02  40400  fiiuncl  45609  gpg5nbgrvtx03starlem1  48654  gpg5nbgrvtx03starlem2  48655  gpg5nbgrvtx03starlem3  48656  gpg5nbgrvtx13starlem1  48657  gpg5nbgrvtx13starlem2  48658  gpg5nbgrvtx13starlem3  48659  gpg5edgnedg  48716  rmsupp0  48954  lcoc0  49008