Theorem neirr 2949

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  neldifsn  4792  frxp2  8169  poxp3  8175  frxp3  8176  ac5b  10518  0nnn  12302  1nuz2  12966  dprd2da  20062  dvlog  26693  legso  28607  hleqnid  28616  umgrnloop0  29126  usgrnloop0ALT  29222  nfrgr2v  30291  0ngrp  30530  neldifpr1  32551  neldifpr2  32552  assafld  33688  signswch  34576  signstfvneq0  34587  linedegen  36144  irrdiff  37327  prtlem400  38871  padd01  39813  padd02  39814  fiiuncl  45070  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  rmsupp0  48284  lcoc0  48339