Theorem neirr 2955

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  neldifsn  4817  frxp2  8185  poxp3  8191  frxp3  8192  ac5b  10547  0nnn  12329  1nuz2  12989  dprd2da  20086  dvlog  26711  legso  28625  hleqnid  28634  umgrnloop0  29144  usgrnloop0ALT  29240  nfrgr2v  30304  0ngrp  30543  neldifpr1  32561  neldifpr2  32562  assafld  33650  signswch  34538  signstfvneq0  34549  linedegen  36107  irrdiff  37292  prtlem400  38826  padd01  39768  padd02  39769  fiiuncl  44967  rmsupp0  48093  lcoc0  48151