Theorem neirr 2942

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

Syntax hints:  ¬ wn 3   = wceq 1542   ≠ wne 2933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  neldifsn  4750  frxp2  8096  poxp3  8102  frxp3  8103  ac5b  10400  0nnn  12193  1nuz2  12849  dprd2da  19985  dvlog  26628  legso  28683  hleqnid  28692  umgrnloop0  29194  usgrnloop0ALT  29290  nfrgr2v  30359  0ngrp  30598  neldifpr1  32619  neldifpr2  32620  assafld  33814  signswch  34738  signstfvneq0  34749  linedegen  36356  irrdiff  37575  prtlem400  39240  padd01  40181  padd02  40182  fiiuncl  45419  gpg5nbgrvtx03starlem1  48422  gpg5nbgrvtx03starlem2  48423  gpg5nbgrvtx03starlem3  48424  gpg5nbgrvtx13starlem1  48425  gpg5nbgrvtx13starlem2  48426  gpg5nbgrvtx13starlem3  48427  gpg5edgnedg  48484  rmsupp0  48722  lcoc0  48776