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

Definition df-ne 2284
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 class 𝐴
2 cB . . 3 class 𝐵
31, 2wne 2283 . 2 wff 𝐴𝐵
41, 2wceq 1314 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 104 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff set class
This definition is referenced by:  neii  2285  neir  2286  nner  2287  nnedc  2288  dcned  2289  neqned  2290  neirr  2292  eqneqall  2293  dcne  2294  nonconne  2295  neeq1  2296  neeq2  2297  neneqd  2304  necon3abii  2319  necon3bii  2321  necon3abid  2322  necon3bid  2324  necon3ad  2325  necon3bd  2326  necon3d  2327  necon3ai  2332  necon3bi  2333  necon1aidc  2334  necon1bidc  2335  necon1idc  2336  necon2ai  2337  necon2ad  2340  necon2bd  2341  necon2d  2342  necon1abiidc  2343  necon1bbiidc  2344  necon1abiddc  2345  necon1bbiddc  2346  necon4aidc  2351  necon4idc  2352  necon4addc  2353  necon4bddc  2354  necon4ddc  2355  necon4abiddc  2356  necon4biddc  2358  necon1addc  2359  necon1bddc  2360  necon1ddc  2361  neanior  2370  ne3anior  2371  nemtbir  2372  nfne  2376  nfned  2377  sbcne12g  2989  dfdif3  3154  ifnefalse  3453  opthpr  3667  prneimg  3669  exmid1dc  4091  onsucelsucexmid  4413  nnsuc  4497  ftpg  5570  fiintim  6783  updjudhf  6930  elni2  7086  indpi  7114  cnstab  8369  nngt1ne1  8712  zapne  9076  prime  9101  elnn1uz2  9350  xrnemnf  9504  xrnepnf  9505  xaddcom  9584  xnegdi  9591  xpncan  9594  xleadd1a  9596  xsubge0  9604  flqeqceilz  10031  ndvdssub  11523  gcdsupex  11542  gcdsupcl  11543  gcdeq0  11561  gcd0id  11563  gcdmultiplez  11605  dvdssq  11615  algcvgblem  11626  lcmdvds  11656  lcmid  11657  mulgcddvds  11671  cncongr2  11681  isprm3  11695  isprm4  11696  sqrt2irr  11736  bdne  12874  exmid1stab  13018
  Copyright terms: Public domain W3C validator