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

Definition df-ne 2203
Description: Define inequality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ne  =/=

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3
2 cB . . 3
31, 2wne 2201 . 2  =/=
41, 2wceq 1242 . . 3
54wn 3 . 2
63, 5wb 98 1  =/=
Colors of variables: wff set class
This definition is referenced by:  neii  2205  neir  2206  nner  2207  nnedc  2208  dcned  2209  neirr  2210  dcne  2211  nonconne  2212  neeq1  2213  neeq2  2214  neneqd  2221  necon3abii  2235  necon3bii  2237  necon3abid  2238  necon3bid  2240  necon3ad  2241  necon3bd  2242  necon3d  2243  necon3ai  2248  necon3bi  2249  necon1aidc  2250  necon1bidc  2251  necon1idc  2252  necon2ai  2253  necon2ad  2256  necon2bd  2257  necon2d  2258  necon1abiidc  2259  necon1bbiidc  2260  necon1abiddc  2261  necon1bbiddc  2262  necon4aidc  2267  necon4idc  2268  necon4addc  2269  necon4bddc  2270  necon4ddc  2271  necon4abiddc  2272  necon4biddc  2274  necon1addc  2275  necon1bddc  2276  necon1ddc  2277  neanior  2286  ne3anior  2287  nemtbir  2288  nfne  2291  nfned  2292  sbcne12g  2862  dfpss2  3023  ifnefalse  3336  opthpr  3534  prneimg  3536  onsucelsucexmid  4215  nnsuc  4281  ftpg  5290  elni2  6298  indpi  6326  nngt1ne1  7709  zapne  8071  prime  8093  elnn1uz2  8300  xrnemnf  8449  xrnepnf  8450  bdne  9288
  Copyright terms: Public domain W3C validator