Theorem neirr 2942

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  neldifsn  4736  frxp2  8087  poxp3  8093  frxp3  8094  ac5b  10391  0nnn  12204  1nuz2  12865  dprd2da  20010  dvlog  26628  legso  28681  hleqnid  28690  umgrnloop0  29192  usgrnloop0ALT  29288  nfrgr2v  30357  0ngrp  30597  neldifpr1  32618  neldifpr2  32619  assafld  33797  signswch  34721  signstfvneq0  34732  linedegen  36341  irrdiff  37656  prtlem400  39330  padd01  40271  padd02  40272  fiiuncl  45514  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg5edgnedg  48618  rmsupp0  48856  lcoc0  48910