Theorem neirr 2947

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

Syntax hints:  ¬ wn 3   = wceq 1537   ≠ wne 2938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ne 2939

This theorem is referenced by:  neldifsn  4797  frxp2  8168  poxp3  8174  frxp3  8175  ac5b  10516  0nnn  12300  1nuz2  12964  dprd2da  20077  dvlog  26708  legso  28622  hleqnid  28631  umgrnloop0  29141  usgrnloop0ALT  29237  nfrgr2v  30301  0ngrp  30540  neldifpr1  32559  neldifpr2  32560  assafld  33665  signswch  34555  signstfvneq0  34566  linedegen  36125  irrdiff  37309  prtlem400  38852  padd01  39794  padd02  39795  fiiuncl  45005  gpg5nbgrvtx03starlem1  47959  gpg5nbgrvtx03starlem2  47960  gpg5nbgrvtx03starlem3  47961  gpg5nbgrvtx13starlem1  47962  gpg5nbgrvtx13starlem2  47963  gpg5nbgrvtx13starlem3  47964  rmsupp0  48213  lcoc0  48268