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

Definition df-ne 2189
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 2187 . 2 wff AB
41, 2wceq 1374 . . 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:  nner  2191  nnedc  2192  neirr  2193  exmidnedc  2194  nonconne  2195  neeq1  2196  neeq2  2197  neneqd  2204  necon3abii  2218  necon3bii  2220  necon3abid  2221  necon3bid  2223  necon3ad  2224  necon3bd  2225  necon3d  2226  necon3ai  2231  necon3bi  2232  necon1aidc  2233  necon1bidc  2234  necon1idc  2235  necon2ai  2236  necon2ad  2239  necon2bd  2240  necon2d  2241  necon1abiidc  2242  necon1bbiidc  2243  necon1abiddc  2244  necon1bbiddc  2245  necon4aidc  2250  necon4idc  2251  necon4addc  2252  necon4bddc  2253  necon4ddc  2254  necon4abiddc  2255  necon4biddc  2257  necon1addc  2258  necon1bddc  2259  necon1ddc  2260  neanior  2269  ne3anior  2270  nemtbir  2271  nfne  2274  nfned  2275  sbcne12g  2845  dfpss2  3008  opthpr  3496  prneimg  3498  onsucelsucexmid  4175  nnsuc  4241  ftpg  5249  elni2  6137
  Copyright terms: Public domain W3C validator