Theorem neirr 2937

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

Syntax hints:  ¬ wn 3   = wceq 1541   ≠ wne 2928

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 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  neldifsn  4741  frxp2  8074  poxp3  8080  frxp3  8081  ac5b  10369  0nnn  12161  1nuz2  12822  dprd2da  19956  dvlog  26587  legso  28577  hleqnid  28586  umgrnloop0  29087  usgrnloop0ALT  29183  nfrgr2v  30252  0ngrp  30491  neldifpr1  32513  neldifpr2  32514  assafld  33650  signswch  34574  signstfvneq0  34585  linedegen  36187  irrdiff  37370  prtlem400  38968  padd01  39909  padd02  39910  fiiuncl  45161  gpg5nbgrvtx03starlem1  48167  gpg5nbgrvtx03starlem2  48168  gpg5nbgrvtx03starlem3  48169  gpg5nbgrvtx13starlem1  48170  gpg5nbgrvtx13starlem2  48171  gpg5nbgrvtx13starlem3  48172  gpg5edgnedg  48229  rmsupp0  48467  lcoc0  48522