|   | 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 2737 | . 2 ⊢ 𝐴 = 𝐴 | |
| 2 | nne 2944 | . 2 ⊢ (¬ 𝐴 ≠ 𝐴 ↔ 𝐴 = 𝐴) | |
| 3 | 1, 2 | mpbir 231 | 1 ⊢ ¬ 𝐴 ≠ 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 = wceq 1540 ≠ wne 2940 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ne 2941 | 
| This theorem is referenced by: neldifsn 4792 frxp2 8169 poxp3 8175 frxp3 8176 ac5b 10518 0nnn 12302 1nuz2 12966 dprd2da 20062 dvlog 26693 legso 28607 hleqnid 28616 umgrnloop0 29126 usgrnloop0ALT 29222 nfrgr2v 30291 0ngrp 30530 neldifpr1 32551 neldifpr2 32552 assafld 33688 signswch 34576 signstfvneq0 34587 linedegen 36144 irrdiff 37327 prtlem400 38871 padd01 39813 padd02 39814 fiiuncl 45070 gpg5nbgrvtx03starlem1 48024 gpg5nbgrvtx03starlem2 48025 gpg5nbgrvtx03starlem3 48026 gpg5nbgrvtx13starlem1 48027 gpg5nbgrvtx13starlem2 48028 gpg5nbgrvtx13starlem3 48029 rmsupp0 48284 lcoc0 48339 | 
| Copyright terms: Public domain | W3C validator |