ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ne Structured version   GIF version

Definition df-ne 2182
Description: Define inequality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ne (AB ↔ ¬ A = B)

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3 class A
2 cB . . 3 class B
31, 2wne 2180 . 2 wff AB
41, 2wceq 1226 . . 3 wff A = B
54wn 3 . 2 wff ¬ A = B
63, 5wb 98 1 wff (AB ↔ ¬ A = B)
Colors of variables: wff set class
This definition is referenced by:  neii  2184  neir  2185  nner  2186  nnedc  2187  neirr  2188  dcne  2189  nonconne  2190  neeq1  2191  neeq2  2192  neneqd  2199  necon3abii  2213  necon3bii  2215  necon3abid  2216  necon3bid  2218  necon3ad  2219  necon3bd  2220  necon3d  2221  necon3ai  2226  necon3bi  2227  necon1aidc  2228  necon1bidc  2229  necon1idc  2230  necon2ai  2231  necon2ad  2234  necon2bd  2235  necon2d  2236  necon1abiidc  2237  necon1bbiidc  2238  necon1abiddc  2239  necon1bbiddc  2240  necon4aidc  2245  necon4idc  2246  necon4addc  2247  necon4bddc  2248  necon4ddc  2249  necon4abiddc  2250  necon4biddc  2252  necon1addc  2253  necon1bddc  2254  necon1ddc  2255  neanior  2264  ne3anior  2265  nemtbir  2266  nfne  2269  nfned  2270  sbcne12g  2839  dfpss2  3000  ifnefalse  3311  opthpr  3509  prneimg  3511  onsucelsucexmid  4190  nnsuc  4256  ftpg  5263  elni2  6163  nngt1ne1  7534  zapne  7886  prime  7905  xrnemnf  8178  xrnepnf  8179  bdne  8430
  Copyright terms: Public domain W3C validator