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

Definition df-ne 2309
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 2308 . 2  wff  A  =/= 
B
41, 2wceq 1331 . . 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  2310  neir  2311  nner  2312  nnedc  2313  dcned  2314  neqned  2315  neirr  2317  eqneqall  2318  dcne  2319  nonconne  2320  neeq1  2321  neeq2  2322  neneqd  2329  necon3abii  2344  necon3bii  2346  necon3abid  2347  necon3bid  2349  necon3ad  2350  necon3bd  2351  necon3d  2352  necon3ai  2357  necon3bi  2358  necon1aidc  2359  necon1bidc  2360  necon1idc  2361  necon2ai  2362  necon2ad  2365  necon2bd  2366  necon2d  2367  necon1abiidc  2368  necon1bbiidc  2369  necon1abiddc  2370  necon1bbiddc  2371  necon4aidc  2376  necon4idc  2377  necon4addc  2378  necon4bddc  2379  necon4ddc  2380  necon4abiddc  2381  necon4biddc  2383  necon1addc  2384  necon1bddc  2385  necon1ddc  2386  neanior  2395  ne3anior  2396  nemtbir  2397  nfne  2401  nfned  2402  sbcne12g  3020  dfdif3  3186  ifnefalse  3485  opthpr  3699  prneimg  3701  exmid1dc  4123  onsucelsucexmid  4445  nnsuc  4529  ftpg  5604  fiintim  6817  updjudhf  6964  elni2  7134  indpi  7162  cnstab  8419  nngt1ne1  8767  zapne  9137  prime  9162  elnn1uz2  9413  xrnemnf  9576  xrnepnf  9577  xaddcom  9656  xnegdi  9663  xpncan  9666  xleadd1a  9668  xsubge0  9676  flqeqceilz  10103  ndvdssub  11638  gcdsupex  11657  gcdsupcl  11658  gcdeq0  11676  gcd0id  11678  gcdmultiplez  11720  dvdssq  11730  algcvgblem  11741  lcmdvds  11771  lcmid  11772  mulgcddvds  11786  cncongr2  11796  isprm3  11810  isprm4  11811  sqrt2irr  11851  bdne  13156  exmid1stab  13300  apdifflemr  13347
  Copyright terms: Public domain W3C validator