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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2708

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-cleq 2729  df-ne 2942

This theorem is referenced by:  neldifsn  4737  ac5b  10307  0nnn  12082  1nuz2  12737  dprd2da  19713  dvlog  25878  legso  27069  hleqnid  27078  umgrnloop0  27588  usgrnloop0ALT  27681  nfrgr2v  28745  0ngrp  28982  neldifpr1  30989  neldifpr2  30990  signswch  32646  signstfvneq0  32657  frxp2  33889  poxp3  33894  frxp3  33895  linedegen  34503  irrdiff  35553  prtlem400  37088  padd01  38030  padd02  38031  fiiuncl  42834  rmsupp0  45956  lcoc0  46015