Theorem neirr 2967

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 2763	. 2 ⊢ 𝐴 = 𝐴
2		nne 2962	. 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴)
3	1, 2	mpbir 234	1 ⊢ ¬ 𝐴 ≠ 𝐴

Syntax hints:  ¬ wn 3   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  pssirr  4058  neldifsn  4761  frxp2  8141  poxp3  8147  frxp3  8148  ac5b  10463  0nnn  12273  1nuz2  12949  dprd2da  20115  dvlog  26794  legso  28846  hleqnid  28858  umgrnloop0  29437  usgrnloop0ALT  29533  nfrgr2v  30601  0ngrp  30841  neldifpr1  32857  neldifpr2  32858  assafld  34005  signswch  34926  signstfvneq0  34937  linedegen  36613  irrdiff  37948  prtlem400  39622  padd01  40563  padd02  40564  fiiuncl  45765  gpg5nbgrvtx03starlem1  48810  gpg5nbgrvtx03starlem2  48811  gpg5nbgrvtx03starlem3  48812  gpg5nbgrvtx13starlem1  48813  gpg5nbgrvtx13starlem2  48814  gpg5nbgrvtx13starlem3  48815  gpg5edgnedg  48872  rmsupp0  49125  lcoc0  49179