Theorem neirr 2832

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 2651	. 2 ⊢ 𝐴 = 𝐴
2		nne 2827	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 221	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1523   ≠ wne 2823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-ne 2824

This theorem is referenced by:  ssdifsn  4351  neldifsn  4354  ac5b  9338  1nuz2  11802  dprd2da  18487  dvlog  24442  legso  25539  hleqnid  25548  umgrnloop0  26049  usgrnloop0ALT  26142  nfrgr2v  27252  0ngrp  27493  signswch  30766  signstfvneq0  30777  linedegen  32375  prtlem400  34474  padd01  35415  padd02  35416  fiiuncl  39548  rmsupp0  42474  lcoc0  42536