Theorem neirr 2970

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

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

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 2156  ax-ext 2738

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

This theorem is used by:  pssirr  4060  neldifsn  4765  frxp2  8149  poxp3  8155  frxp3  8156  ac5b  10480  0nnn  12290  1nuz2  12966  dprd2da  20145  dvlog  26853  legso  28905  hleqnid  28917  umgrnloop0  29496  usgrnloop0ALT  29592  nfrgr2v  30660  0ngrp  30900  neldifpr1  32916  neldifpr2  32917  assafld  34058  signswch  34980  signstfvneq0  34991  linedegen  36656  irrdiff  38011  prtlem400  39685  padd01  40626  padd02  40627  fiiuncl  45826  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpg5edgnedg  48936  rmsupp0  49189  lcoc0  49243