New Foundations Explorer		< Previous   Next > Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ne		Unicode version

---

Definition df-ne 2518

Description: Define inequality. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
df-ne

---

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3
2		cB	. . 3
3	1, 2	wne 2516	. 2
4	1, 2	wceq 1642	. . 3
5	4	wn 3	. 2
6	3, 5	wb 176	1

Colors of variables: wff setvar class

This definition is referenced by:  nne  2520  exmidne  2522  nonconne  2523  neeq1  2524  neeq2  2525  neneqd  2532  necon3abii  2546  necon3bii  2548  necon3abid  2549  necon3bid  2551  necon3d  2554  necon1ai  2558  necon1i  2560  necon2bd  2565  necon2d  2566  necon1abii  2567  necon1bbii  2568  necon1abid  2569  necon1bbid  2570  necon2abid  2573  necon2bbid  2574  necon4abid  2580  necon1ad  2583  neor  2600  neanior  2601  neorian  2603  nemtbir  2604  nfne  2610  nfned  2612  dfpss2  3354  ne0i  3556  neq0  3560  ab0  3569  ifnefalse  3670  eqsn  3867  snsssn  3873  unissint  3950  iununi  4050  0cnsuc  4401  nnsucelrlem2  4425  nnsucelrlem3  4426  nndisjeq  4429  preaddccan2lem1  4454  ltfinirr  4457  ltfinex  4464  ltfintrilem1  4465  tfinprop  4489  tfinltfin  4501  evenfinex  4503  oddfinex  4504  evenoddnnnul  4514  evenodddisjlem1  4515  evenodddisj  4516  sfinltfin  4535  vfinncvntnn  4548  vfinncvntsp  4549  nulnnn  4556  0cnelphi  4597  imasn  5018  xpcan  5057  xpcan2  5058  nfunv  5138  xpnedisj  5513  enprmaplem5  6080  fce  6188  el2c  6191  ncslemuc  6255  ncvsq  6256  0lt1c  6258  nnc3n3p1  6278  nchoicelem9  6297  nchoicelem12  6300  nchoicelem14  6302  fnfreclem2  6318  fnfreclem3  6319

Copyright terms: Public domain

W3C validator