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 2818 | . 2 ⊢ 𝐴 = 𝐴 | |
2 | nne 3017 | . 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴) | |
3 | 1, 2 | mpbir 232 | 1 ⊢ ¬ 𝐴 ≠ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 = wceq 1528 ≠ wne 3013 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-ne 3014 |
This theorem is referenced by: neldifsn 4717 ac5b 9888 0nnn 11661 1nuz2 12312 dprd2da 19093 dvlog 25161 legso 26312 hleqnid 26321 umgrnloop0 26821 usgrnloop0ALT 26914 nfrgr2v 27978 0ngrp 28215 neldifpr1 30220 neldifpr2 30221 signswch 31730 signstfvneq0 31741 linedegen 33501 prtlem400 35886 padd01 36827 padd02 36828 fiiuncl 41204 rmsupp0 44344 lcoc0 44405 |
Copyright terms: Public domain | W3C validator |