Theorem neirr 2968

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  pssirr  4033  neldifsn  4755  frxp2  8188  poxp3  8194  frxp3  8195  ac5b  10583  0nnn  12401  1nuz2  13078  dprd2da  20288  dvlog  27009  legso  29092  hleqnid  29104  umgrnloop0  29717  usgrnloop0ALT  29816  nfrgr2v  30903  0ngrp  31143  neldifpr1  33201  neldifpr2  33202  assafld  34339  signswch  35260  signstfvneq0  35271  linedegen  37086  irrdiff  38439  prtlem400  40119  padd01  41060  padd02  41061  fiiuncl  46287  gpg5nbgrvtx03starlem1  49371  gpg5nbgrvtx03starlem2  49372  gpg5nbgrvtx03starlem3  49373  gpg5nbgrvtx13starlem1  49374  gpg5nbgrvtx13starlem2  49375  gpg5nbgrvtx13starlem3  49376  gpg5edgnedg  49433  rmsupp0  49685  lcoc0  49739