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

Definition df-ne 2188
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 2186 . 2 wff AB
41, 2wceq 1228 . . 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  2190  neir  2191  nner  2192  nnedc  2193  neirr  2194  exmidnedc  2195  nonconne  2196  neeq1  2197  neeq2  2198  neneqd  2205  necon3abii  2219  necon3bii  2221  necon3abid  2222  necon3bid  2224  necon3ad  2225  necon3bd  2226  necon3d  2227  necon3ai  2232  necon3bi  2233  necon1aidc  2234  necon1bidc  2235  necon1idc  2236  necon2ai  2237  necon2ad  2240  necon2bd  2241  necon2d  2242  necon1abiidc  2243  necon1bbiidc  2244  necon1abiddc  2245  necon1bbiddc  2246  necon4aidc  2251  necon4idc  2252  necon4addc  2253  necon4bddc  2254  necon4ddc  2255  necon4abiddc  2256  necon4biddc  2258  necon1addc  2259  necon1bddc  2260  necon1ddc  2261  neanior  2270  ne3anior  2271  nemtbir  2272  nfne  2275  nfned  2276  sbcne12g  2845  dfpss2  3006  ifnefalse  3319  opthpr  3517  prneimg  3519  onsucelsucexmid  4199  nnsuc  4265  ftpg  5272  elni2  6174  bdne  7080
  Copyright terms: Public domain W3C validator