ILE Home 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  neirr  2213  dcne  2214  nonconne  2215  neeq1  2216  neeq2  2217  neneqd  2224  necon3abii  2238  necon3bii  2240  necon3abid  2241  necon3bid  2243  necon3ad  2244  necon3bd  2245  necon3d  2246  necon3ai  2251  necon3bi  2252  necon1aidc  2253  necon1bidc  2254  necon1idc  2255  necon2ai  2256  necon2ad  2259  necon2bd  2260  necon2d  2261  necon1abiidc  2262  necon1bbiidc  2263  necon1abiddc  2264  necon1bbiddc  2265  necon4aidc  2270  necon4idc  2271  necon4addc  2272  necon4bddc  2273  necon4ddc  2274  necon4abiddc  2275  necon4biddc  2277  necon1addc  2278  necon1bddc  2279  necon1ddc  2280  neanior  2289  ne3anior  2290  nemtbir  2291  nfne  2294  nfned  2295  sbcne12g  2865  dfpss2  3026  ifnefalse  3339  opthpr  3540  prneimg  3542  onsucelsucexmid  4242  nnsuc  4316  ftpg  5325  elni2  6384  indpi  6412  nngt1ne1  7915  zapne  8278  prime  8300  elnn1uz2  8507  xrnemnf  8657  xrnepnf  8658  sqrt2irr  9746  algcvgblem  9756  bdne  9837
  Copyright terms: Public domain W3C validator