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

Definition df-ne 2247
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 2246 . 2 wff 𝐴𝐵
41, 2wceq 1285 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 103 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff set class
This definition is referenced by:  neii  2248  neir  2249  nner  2250  nnedc  2251  dcned  2252  neqned  2253  neirr  2255  eqneqall  2256  dcne  2257  nonconne  2258  neeq1  2259  neeq2  2260  neneqd  2267  necon3abii  2282  necon3bii  2284  necon3abid  2285  necon3bid  2287  necon3ad  2288  necon3bd  2289  necon3d  2290  necon3ai  2295  necon3bi  2296  necon1aidc  2297  necon1bidc  2298  necon1idc  2299  necon2ai  2300  necon2ad  2303  necon2bd  2304  necon2d  2305  necon1abiidc  2306  necon1bbiidc  2307  necon1abiddc  2308  necon1bbiddc  2309  necon4aidc  2314  necon4idc  2315  necon4addc  2316  necon4bddc  2317  necon4ddc  2318  necon4abiddc  2319  necon4biddc  2321  necon1addc  2322  necon1bddc  2323  necon1ddc  2324  neanior  2333  ne3anior  2334  nemtbir  2335  nfne  2338  nfned  2339  sbcne12g  2925  ifnefalse  3364  opthpr  3566  prneimg  3568  onsucelsucexmid  4275  nnsuc  4358  ftpg  5373  elni2  6555  indpi  6583  nngt1ne1  8129  zapne  8492  prime  8516  elnn1uz2  8764  xrnemnf  8918  xrnepnf  8919  flqeqceilz  9389  ndvdssub  10463  gcdsupex  10482  gcdsupcl  10483  gcdeq0  10501  gcd0id  10503  gcdmultiplez  10543  dvdssq  10553  algcvgblem  10564  lcmdvds  10594  lcmid  10595  mulgcddvds  10609  cncongr2  10619  isprm3  10633  isprm4  10634  sqrt2irr  10674  bdne  10787
  Copyright terms: Public domain W3C validator