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

Definition df-ne 2250
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 2249 . 2  wff  A  =/= 
B
41, 2wceq 1285 . . 3  wff  A  =  B
54wn 3 . 2  wff  -.  A  =  B
63, 5wb 103 1  wff  ( A  =/=  B  <->  -.  A  =  B )
Colors of variables: wff set class
This definition is referenced by:  neii  2251  neir  2252  nner  2253  nnedc  2254  dcned  2255  neqned  2256  neirr  2258  eqneqall  2259  dcne  2260  nonconne  2261  neeq1  2262  neeq2  2263  neneqd  2270  necon3abii  2285  necon3bii  2287  necon3abid  2288  necon3bid  2290  necon3ad  2291  necon3bd  2292  necon3d  2293  necon3ai  2298  necon3bi  2299  necon1aidc  2300  necon1bidc  2301  necon1idc  2302  necon2ai  2303  necon2ad  2306  necon2bd  2307  necon2d  2308  necon1abiidc  2309  necon1bbiidc  2310  necon1abiddc  2311  necon1bbiddc  2312  necon4aidc  2317  necon4idc  2318  necon4addc  2319  necon4bddc  2320  necon4ddc  2321  necon4abiddc  2322  necon4biddc  2324  necon1addc  2325  necon1bddc  2326  necon1ddc  2327  neanior  2336  ne3anior  2337  nemtbir  2338  nfne  2342  nfned  2343  sbcne12g  2935  dfdif3  3094  ifnefalse  3384  opthpr  3590  prneimg  3592  onsucelsucexmid  4308  nnsuc  4392  ftpg  5421  updjudhf  6675  elni2  6774  indpi  6802  nngt1ne1  8348  zapne  8715  prime  8739  elnn1uz2  8987  xrnemnf  9141  xrnepnf  9142  flqeqceilz  9612  ndvdssub  10708  gcdsupex  10727  gcdsupcl  10728  gcdeq0  10746  gcd0id  10748  gcdmultiplez  10788  dvdssq  10798  algcvgblem  10809  lcmdvds  10839  lcmid  10840  mulgcddvds  10854  cncongr2  10864  isprm3  10878  isprm4  10879  sqrt2irr  10919  bdne  11085
  Copyright terms: Public domain W3C validator