Theorem neirr 2965

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ne 2957

This theorem is used by:  pssirr  4051  neldifsn  4755  frxp2  8145  poxp3  8151  frxp3  8152  ac5b  10537  0nnn  12355  1nuz2  13032  dprd2da  20238  dvlog  26961  legso  29044  hleqnid  29056  umgrnloop0  29669  usgrnloop0ALT  29768  nfrgr2v  30855  0ngrp  31095  neldifpr1  33111  neldifpr2  33112  assafld  34251  signswch  35173  signstfvneq0  35184  linedegen  36878  irrdiff  38215  prtlem400  39895  padd01  40836  padd02  40837  fiiuncl  46025  gpg5nbgrvtx03starlem1  49110  gpg5nbgrvtx03starlem2  49111  gpg5nbgrvtx03starlem3  49112  gpg5nbgrvtx13starlem1  49113  gpg5nbgrvtx13starlem2  49114  gpg5nbgrvtx13starlem3  49115  gpg5edgnedg  49172  rmsupp0  49424  lcoc0  49478