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

Definition df-ne 2286
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 2285 . 2  wff  A  =/= 
B
41, 2wceq 1316 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 104 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  neii  2287  neir  2288  nner  2289  nnedc  2290  dcned  2291  neqned  2292  neirr  2294  eqneqall  2295  dcne  2296  nonconne  2297  neeq1  2298  neeq2  2299  neneqd  2306  necon3abii  2321  necon3bii  2323  necon3abid  2324  necon3bid  2326  necon3ad  2327  necon3bd  2328  necon3d  2329  necon3ai  2334  necon3bi  2335  necon1aidc  2336  necon1bidc  2337  necon1idc  2338  necon2ai  2339  necon2ad  2342  necon2bd  2343  necon2d  2344  necon1abiidc  2345  necon1bbiidc  2346  necon1abiddc  2347  necon1bbiddc  2348  necon4aidc  2353  necon4idc  2354  necon4addc  2355  necon4bddc  2356  necon4ddc  2357  necon4abiddc  2358  necon4biddc  2360  necon1addc  2361  necon1bddc  2362  necon1ddc  2363  neanior  2372  ne3anior  2373  nemtbir  2374  nfne  2378  nfned  2379  sbcne12g  2991  dfdif3  3156  ifnefalse  3455  opthpr  3669  prneimg  3671  exmid1dc  4093  onsucelsucexmid  4415  nnsuc  4499  ftpg  5572  fiintim  6785  updjudhf  6932  elni2  7090  indpi  7118  cnstab  8374  nngt1ne1  8719  zapne  9083  prime  9108  elnn1uz2  9357  xrnemnf  9519  xrnepnf  9520  xaddcom  9599  xnegdi  9606  xpncan  9609  xleadd1a  9611  xsubge0  9619  flqeqceilz  10046  ndvdssub  11539  gcdsupex  11558  gcdsupcl  11559  gcdeq0  11577  gcd0id  11579  gcdmultiplez  11621  dvdssq  11631  algcvgblem  11642  lcmdvds  11672  lcmid  11673  mulgcddvds  11687  cncongr2  11697  isprm3  11711  isprm4  11712  sqrt2irr  11752  bdne  12947  exmid1stab  13091
  Copyright terms: Public domain W3C validator