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

Definition df-ne 2252
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 2251 . 2 wff 𝐴𝐵
41, 2wceq 1287 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 103 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff set class
This definition is referenced by:  neii  2253  neir  2254  nner  2255  nnedc  2256  dcned  2257  neqned  2258  neirr  2260  eqneqall  2261  dcne  2262  nonconne  2263  neeq1  2264  neeq2  2265  neneqd  2272  necon3abii  2287  necon3bii  2289  necon3abid  2290  necon3bid  2292  necon3ad  2293  necon3bd  2294  necon3d  2295  necon3ai  2300  necon3bi  2301  necon1aidc  2302  necon1bidc  2303  necon1idc  2304  necon2ai  2305  necon2ad  2308  necon2bd  2309  necon2d  2310  necon1abiidc  2311  necon1bbiidc  2312  necon1abiddc  2313  necon1bbiddc  2314  necon4aidc  2319  necon4idc  2320  necon4addc  2321  necon4bddc  2322  necon4ddc  2323  necon4abiddc  2324  necon4biddc  2326  necon1addc  2327  necon1bddc  2328  necon1ddc  2329  neanior  2338  ne3anior  2339  nemtbir  2340  nfne  2344  nfned  2345  sbcne12g  2938  dfdif3  3099  ifnefalse  3390  opthpr  3601  prneimg  3603  onsucelsucexmid  4321  nnsuc  4405  ftpg  5446  updjudhf  6717  elni2  6820  indpi  6848  nngt1ne1  8394  zapne  8757  prime  8781  elnn1uz2  9029  xrnemnf  9183  xrnepnf  9184  flqeqceilz  9656  ndvdssub  10836  gcdsupex  10855  gcdsupcl  10856  gcdeq0  10874  gcd0id  10876  gcdmultiplez  10916  dvdssq  10926  algcvgblem  10937  lcmdvds  10967  lcmid  10968  mulgcddvds  10982  cncongr2  10992  isprm3  11006  isprm4  11007  sqrt2irr  11047  bdne  11213
  Copyright terms: Public domain W3C validator