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

Definition df-ne 2206
 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 2204 . 2 wff 𝐴𝐵
41, 2wceq 1243 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 98 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
 Colors of variables: wff set class This definition is referenced by:  neii  2208  neir  2209  nner  2210  nnedc  2211  dcned  2212  neqned  2213  neirr  2215  dcne  2216  nonconne  2217  neeq1  2218  neeq2  2219  neneqd  2226  necon3abii  2241  necon3bii  2243  necon3abid  2244  necon3bid  2246  necon3ad  2247  necon3bd  2248  necon3d  2249  necon3ai  2254  necon3bi  2255  necon1aidc  2256  necon1bidc  2257  necon1idc  2258  necon2ai  2259  necon2ad  2262  necon2bd  2263  necon2d  2264  necon1abiidc  2265  necon1bbiidc  2266  necon1abiddc  2267  necon1bbiddc  2268  necon4aidc  2273  necon4idc  2274  necon4addc  2275  necon4bddc  2276  necon4ddc  2277  necon4abiddc  2278  necon4biddc  2280  necon1addc  2281  necon1bddc  2282  necon1ddc  2283  neanior  2292  ne3anior  2293  nemtbir  2294  nfne  2297  nfned  2298  sbcne12g  2868  dfpss2  3029  ifnefalse  3342  opthpr  3543  prneimg  3545  onsucelsucexmid  4255  nnsuc  4338  ftpg  5347  elni2  6412  indpi  6440  nngt1ne1  7948  zapne  8315  prime  8337  elnn1uz2  8544  xrnemnf  8699  xrnepnf  8700  flqeqceilz  9160  sqrt2irr  9878  algcvgblem  9888  bdne  9973
 Copyright terms: Public domain W3C validator