Theorem neirr 2941

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

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ne 2933

This theorem is referenced by:  neldifsn  4768  frxp2  8143  poxp3  8149  frxp3  8150  ac5b  10492  0nnn  12276  1nuz2  12940  dprd2da  20025  dvlog  26612  legso  28578  hleqnid  28587  umgrnloop0  29088  usgrnloop0ALT  29184  nfrgr2v  30253  0ngrp  30492  neldifpr1  32514  neldifpr2  32515  assafld  33677  signswch  34593  signstfvneq0  34604  linedegen  36161  irrdiff  37344  prtlem400  38888  padd01  39830  padd02  39831  fiiuncl  45089  gpg5nbgrvtx03starlem1  48070  gpg5nbgrvtx03starlem2  48071  gpg5nbgrvtx03starlem3  48072  gpg5nbgrvtx13starlem1  48073  gpg5nbgrvtx13starlem2  48074  gpg5nbgrvtx13starlem3  48075  rmsupp0  48343  lcoc0  48398