![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neirr | Structured version Visualization version GIF version |
Description: No class is unequal to itself. Inequality is irreflexive. (Contributed by Stefan O'Rear, 1-Jan-2015.) |
Ref | Expression |
---|---|
neirr | ⊢ ¬ 𝐴 ≠ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2760 | . 2 ⊢ 𝐴 = 𝐴 | |
2 | nne 2936 | . 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴) | |
3 | 1, 2 | mpbir 221 | 1 ⊢ ¬ 𝐴 ≠ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1632 ≠ wne 2932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 df-ne 2933 |
This theorem is referenced by: ssdifsnOLD 4464 neldifsn 4467 ac5b 9492 1nuz2 11957 dprd2da 18641 dvlog 24596 legso 25693 hleqnid 25702 umgrnloop0 26203 usgrnloop0ALT 26296 nfrgr2v 27426 0ngrp 27674 signswch 30947 signstfvneq0 30958 linedegen 32556 prtlem400 34659 padd01 35600 padd02 35601 fiiuncl 39733 rmsupp0 42659 lcoc0 42721 |
Copyright terms: Public domain | W3C validator |