Theorem neirr 2969

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

Syntax hints:  ¬ wn 3   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  pssirr  4059  neldifsn  4755  frxp2  8128  poxp3  8134  frxp3  8135  ac5b  10450  0nnn  12263  1nuz2  12939  dprd2da  20105  dvlog  26774  legso  28826  hleqnid  28835  umgrnloop0  29368  usgrnloop0ALT  29464  nfrgr2v  30532  0ngrp  30772  neldifpr1  32789  neldifpr2  32790  assafld  33944  signswch  34865  signstfvneq0  34876  linedegen  36506  irrdiff  37830  prtlem400  39506  padd01  40447  padd02  40448  fiiuncl  45643  gpg5nbgrvtx03starlem1  48688  gpg5nbgrvtx03starlem2  48689  gpg5nbgrvtx03starlem3  48690  gpg5nbgrvtx13starlem1  48691  gpg5nbgrvtx13starlem2  48692  gpg5nbgrvtx13starlem3  48693  gpg5edgnedg  48750  rmsupp0  48999  lcoc0  49053