Theorem neirr 2950

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

Syntax hints:  ¬ wn 3   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  neldifsn  4796  frxp2  8130  poxp3  8136  frxp3  8137  ac5b  10473  0nnn  12248  1nuz2  12908  dprd2da  19912  dvlog  26159  legso  27850  hleqnid  27859  umgrnloop0  28369  usgrnloop0ALT  28462  nfrgr2v  29525  0ngrp  29764  neldifpr1  31770  neldifpr2  31771  signswch  33572  signstfvneq0  33583  linedegen  35115  irrdiff  36207  prtlem400  37740  padd01  38682  padd02  38683  fiiuncl  43752  rmsupp0  47044  lcoc0  47103