Theorem neirr 2952

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

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

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  neldifsn  4725  ac5b  10234  0nnn  12009  1nuz2  12664  dprd2da  19645  dvlog  25806  legso  26960  hleqnid  26969  umgrnloop0  27479  usgrnloop0ALT  27572  nfrgr2v  28636  0ngrp  28873  neldifpr1  30881  neldifpr2  30882  signswch  32540  signstfvneq0  32551  frxp2  33791  poxp3  33796  frxp3  33797  linedegen  34445  irrdiff  35497  prtlem400  36884  padd01  37825  padd02  37826  fiiuncl  42613  rmsupp0  45704  lcoc0  45763