Theorem neirr 2964

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 2760	. 2 ⊢ 𝐴 = 𝐴
2		nne 2959	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 234	1 ⊢ ¬ 𝐴 ≠ 𝐴

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  pssirr  4030  neldifsn  4751  frxp2  8163  poxp3  8169  frxp3  8170  ac5b  10559  0nnn  12377  1nuz2  13054  dprd2da  20263  dvlog  26984  legso  29067  hleqnid  29079  umgrnloop0  29692  usgrnloop0ALT  29791  nfrgr2v  30878  0ngrp  31118  neldifpr1  33176  neldifpr2  33177  assafld  34315  signswch  35236  signstfvneq0  35247  linedegen  37000  irrdiff  38340  prtlem400  40020  padd01  40961  padd02  40962  fiiuncl  46175  gpg5nbgrvtx03starlem1  49259  gpg5nbgrvtx03starlem2  49260  gpg5nbgrvtx03starlem3  49261  gpg5nbgrvtx13starlem1  49262  gpg5nbgrvtx13starlem2  49263  gpg5nbgrvtx13starlem3  49264  gpg5edgnedg  49321  rmsupp0  49573  lcoc0  49627