Theorem neirr 2938

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

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

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 2123  ax-ext 2705

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

This theorem is referenced by:  neldifsn  4743  frxp2  8080  poxp3  8086  frxp3  8087  ac5b  10376  0nnn  12168  1nuz2  12824  dprd2da  19958  dvlog  26588  legso  28578  hleqnid  28587  umgrnloop0  29089  usgrnloop0ALT  29185  nfrgr2v  30254  0ngrp  30493  neldifpr1  32515  neldifpr2  32516  assafld  33671  signswch  34595  signstfvneq0  34606  linedegen  36208  irrdiff  37391  prtlem400  38989  padd01  39930  padd02  39931  fiiuncl  45186  gpg5nbgrvtx03starlem1  48192  gpg5nbgrvtx03starlem2  48193  gpg5nbgrvtx03starlem3  48194  gpg5nbgrvtx13starlem1  48195  gpg5nbgrvtx13starlem2  48196  gpg5nbgrvtx13starlem3  48197  gpg5edgnedg  48254  rmsupp0  48492  lcoc0  48547