Theorem neirr 2944

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 2740	. 2 ⊢ 𝐴 = 𝐴
2		nne 2939	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 232	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  neldifsn  4732  frxp2  8091  poxp3  8097  frxp3  8098  ac5b  10398  0nnn  12211  1nuz2  12872  dprd2da  20017  dvlog  26640  legso  28692  hleqnid  28701  umgrnloop0  29203  usgrnloop0ALT  29299  nfrgr2v  30367  0ngrp  30607  neldifpr1  32628  neldifpr2  32629  assafld  33828  signswch  34752  signstfvneq0  34763  linedegen  36378  irrdiff  37693  prtlem400  39369  padd01  40310  padd02  40311  fiiuncl  45520  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg5edgnedg  48628  rmsupp0  48866  lcoc0  48920