Theorem neirr 2934

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  neldifsn  4756  frxp2  8123  poxp3  8129  frxp3  8130  ac5b  10431  0nnn  12222  1nuz2  12883  dprd2da  19974  dvlog  26560  legso  28526  hleqnid  28535  umgrnloop0  29036  usgrnloop0ALT  29132  nfrgr2v  30201  0ngrp  30440  neldifpr1  32462  neldifpr2  32463  assafld  33633  signswch  34552  signstfvneq0  34563  linedegen  36131  irrdiff  37314  prtlem400  38863  padd01  39805  padd02  39806  fiiuncl  45059  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  rmsupp0  48356  lcoc0  48411