Definition df-ne 2404

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 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	wne 2403	. 2 wff 𝐴 ≠ 𝐵
4	1, 2	wceq 1398	. . 3 wff 𝐴 = 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 = 𝐵
6	3, 5	wb 105	1 wff (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)

This definition is referenced by:  neii  2405  neir  2406  nner  2407  nnedc  2408  dcned  2409  neqned  2410  neirr  2412  eqneqall  2413  dcne  2414  nonconne  2415  neeq1  2416  neeq2  2417  neneqd  2424  necon3abii  2439  necon3bii  2441  necon3abid  2442  necon3bid  2444  necon3ad  2445  necon3bd  2446  necon3d  2447  necon3ai  2452  necon3bi  2453  necon1aidc  2454  necon1bidc  2455  necon1idc  2456  necon2ai  2457  necon2ad  2460  necon2bd  2461  necon2d  2462  necon1abiidc  2463  necon1bbiidc  2464  necon1abiddc  2465  necon1bbiddc  2466  necon4aidc  2471  necon4idc  2472  necon4addc  2473  necon4bddc  2474  necon4ddc  2475  necon4abiddc  2476  necon4biddc  2478  necon1addc  2479  necon1bddc  2480  necon1ddc  2481  neanior  2490  ne3anior  2491  nemtbir  2492  nfne  2496  nfned  2497  sbcne12g  3146  dfdif3  3319  ifnefalse  3620  opthpr  3860  prneimg  3862  exmid1dc  4296  exmid1stab  4304  onsucelsucexmid  4634  nnsuc  4720  ftpg  5846  fvdifsuppst  6422  suppssrst  6439  suppssrgst  6440  fiintim  7166  updjudhf  7321  netap  7516  elni2  7577  indpi  7605  nngt1ne1  9221  zapne  9599  prime  9624  elnn1uz2  9886  xrnemnf  10057  xrnepnf  10058  xaddcom  10141  xnegdi  10148  xpncan  10151  xleadd1a  10153  xsubge0  10161  flqeqceilz  10626  ndvdssub  12554  gcdsupex  12591  gcdsupcl  12592  gcdeq0  12611  gcd0id  12613  gcdmultiplez  12655  dvdssq  12665  algcvgblem  12684  lcmdvds  12714  lcmid  12715  mulgcddvds  12729  cncongr2  12739  isprm3  12753  isprm4  12754  sqrt2irr  12797  pcxcl  12947  isnzr2  14262  lgscllem  15809  umgr2edg1  16133  eupth2lem1  16382  eupth2lem3lem4fi  16397  bdne  16552  apdifflemr  16762