Theorem neirr 2951

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 2738	. 2 ⊢ 𝐴 = 𝐴
2		nne 2946	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 230	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  neldifsn  4722  ac5b  10165  0nnn  11939  1nuz2  12593  dprd2da  19560  dvlog  25711  legso  26864  hleqnid  26873  umgrnloop0  27382  usgrnloop0ALT  27475  nfrgr2v  28537  0ngrp  28774  neldifpr1  30782  neldifpr2  30783  signswch  32440  signstfvneq0  32451  frxp2  33718  poxp3  33723  frxp3  33724  linedegen  34372  irrdiff  35424  prtlem400  36811  padd01  37752  padd02  37753  fiiuncl  42502  rmsupp0  45592  lcoc0  45651