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

Definition df-ne 2221
Description: Define inequality. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-ne  |-  ( A  =/=  B  <->  -.  A  =  B )

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3  class  A
2 cB . . 3  class  B
31, 2wne 2220 . 2  wff  A  =/= 
B
41, 2wceq 1259 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 102 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  neii  2222  neir  2223  nner  2224  nnedc  2225  dcned  2226  neqned  2227  neirr  2229  eqneqall  2230  dcne  2231  nonconne  2232  neeq1  2233  neeq2  2234  neneqd  2241  necon3abii  2256  necon3bii  2258  necon3abid  2259  necon3bid  2261  necon3ad  2262  necon3bd  2263  necon3d  2264  necon3ai  2269  necon3bi  2270  necon1aidc  2271  necon1bidc  2272  necon1idc  2273  necon2ai  2274  necon2ad  2277  necon2bd  2278  necon2d  2279  necon1abiidc  2280  necon1bbiidc  2281  necon1abiddc  2282  necon1bbiddc  2283  necon4aidc  2288  necon4idc  2289  necon4addc  2290  necon4bddc  2291  necon4ddc  2292  necon4abiddc  2293  necon4biddc  2295  necon1addc  2296  necon1bddc  2297  necon1ddc  2298  neanior  2307  ne3anior  2308  nemtbir  2309  nfne  2312  nfned  2313  sbcne12g  2895  dfpss2  3056  ifnefalse  3369  opthpr  3570  prneimg  3572  onsucelsucexmid  4282  nnsuc  4365  ftpg  5374  elni2  6469  indpi  6497  nngt1ne1  8023  zapne  8372  prime  8395  elnn1uz2  8640  xrnemnf  8799  xrnepnf  8800  flqeqceilz  9267  sqrt2irr  10230  algcvgblem  10250  bdne  10339
  Copyright terms: Public domain W3C validator