Definition df-ne 2377

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

Assertion

Ref	Expression
df-ne	|- ( A =/= B <-> -. A = B )

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wne 2376	. 2 wff A =/= B
4	1, 2	wceq 1373	. . 3 wff A = B
5	4	wn 3	. 2 wff -. A = B
6	3, 5	wb 105	1 wff ( A =/= B <-> -. A = B )

This definition is referenced by:  neii  2378  neir  2379  nner  2380  nnedc  2381  dcned  2382  neqned  2383  neirr  2385  eqneqall  2386  dcne  2387  nonconne  2388  neeq1  2389  neeq2  2390  neneqd  2397  necon3abii  2412  necon3bii  2414  necon3abid  2415  necon3bid  2417  necon3ad  2418  necon3bd  2419  necon3d  2420  necon3ai  2425  necon3bi  2426  necon1aidc  2427  necon1bidc  2428  necon1idc  2429  necon2ai  2430  necon2ad  2433  necon2bd  2434  necon2d  2435  necon1abiidc  2436  necon1bbiidc  2437  necon1abiddc  2438  necon1bbiddc  2439  necon4aidc  2444  necon4idc  2445  necon4addc  2446  necon4bddc  2447  necon4ddc  2448  necon4abiddc  2449  necon4biddc  2451  necon1addc  2452  necon1bddc  2453  necon1ddc  2454  neanior  2463  ne3anior  2464  nemtbir  2465  nfne  2469  nfned  2470  sbcne12g  3111  dfdif3  3283  ifnefalse  3582  opthpr  3813  prneimg  3815  exmid1dc  4245  exmid1stab  4253  onsucelsucexmid  4579  nnsuc  4665  ftpg  5770  fiintim  7030  updjudhf  7183  netap  7368  elni2  7429  indpi  7457  nngt1ne1  9073  zapne  9449  prime  9474  elnn1uz2  9730  xrnemnf  9901  xrnepnf  9902  xaddcom  9985  xnegdi  9992  xpncan  9995  xleadd1a  9997  xsubge0  10005  flqeqceilz  10465  ndvdssub  12274  gcdsupex  12311  gcdsupcl  12312  gcdeq0  12331  gcd0id  12333  gcdmultiplez  12375  dvdssq  12385  algcvgblem  12404  lcmdvds  12434  lcmid  12435  mulgcddvds  12449  cncongr2  12459  isprm3  12473  isprm4  12474  sqrt2irr  12517  pcxcl  12667  isnzr2  13979  lgscllem  15517  bdne  15826  apdifflemr  16023