Theorem neirr 2966

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  pssirr  4054  neldifsn  4758  frxp2  8146  poxp3  8152  frxp3  8153  ac5b  10484  0nnn  12300  1nuz2  12977  dprd2da  20177  dvlog  26896  legso  28949  hleqnid  28961  umgrnloop0  29574  usgrnloop0ALT  29673  nfrgr2v  30760  0ngrp  31000  neldifpr1  33016  neldifpr2  33017  assafld  34155  signswch  35077  signstfvneq0  35088  linedegen  36731  irrdiff  38086  prtlem400  39751  padd01  40692  padd02  40693  fiiuncl  45907  gpg5nbgrvtx03starlem1  48992  gpg5nbgrvtx03starlem2  48993  gpg5nbgrvtx03starlem3  48994  gpg5nbgrvtx13starlem1  48995  gpg5nbgrvtx13starlem2  48996  gpg5nbgrvtx13starlem3  48997  gpg5edgnedg  49054  rmsupp0  49306  lcoc0  49360