Definition df-ne 2403

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

This definition is referenced by:  neii  2404  neir  2405  nner  2406  nnedc  2407  dcned  2408  neqned  2409  neirr  2411  eqneqall  2412  dcne  2413  nonconne  2414  neeq1  2415  neeq2  2416  neneqd  2423  necon3abii  2438  necon3bii  2440  necon3abid  2441  necon3bid  2443  necon3ad  2444  necon3bd  2445  necon3d  2446  necon3ai  2451  necon3bi  2452  necon1aidc  2453  necon1bidc  2454  necon1idc  2455  necon2ai  2456  necon2ad  2459  necon2bd  2460  necon2d  2461  necon1abiidc  2462  necon1bbiidc  2463  necon1abiddc  2464  necon1bbiddc  2465  necon4aidc  2470  necon4idc  2471  necon4addc  2472  necon4bddc  2473  necon4ddc  2474  necon4abiddc  2475  necon4biddc  2477  necon1addc  2478  necon1bddc  2479  necon1ddc  2480  neanior  2489  ne3anior  2490  nemtbir  2491  nfne  2495  nfned  2496  sbcne12g  3145  dfdif3  3317  ifnefalse  3616  opthpr  3855  prneimg  3857  exmid1dc  4290  exmid1stab  4298  onsucelsucexmid  4628  nnsuc  4714  ftpg  5837  fiintim  7122  updjudhf  7277  netap  7472  elni2  7533  indpi  7561  nngt1ne1  9177  zapne  9553  prime  9578  elnn1uz2  9840  xrnemnf  10011  xrnepnf  10012  xaddcom  10095  xnegdi  10102  xpncan  10105  xleadd1a  10107  xsubge0  10115  flqeqceilz  10579  ndvdssub  12490  gcdsupex  12527  gcdsupcl  12528  gcdeq0  12547  gcd0id  12549  gcdmultiplez  12591  dvdssq  12601  algcvgblem  12620  lcmdvds  12650  lcmid  12651  mulgcddvds  12665  cncongr2  12675  isprm3  12689  isprm4  12690  sqrt2irr  12733  pcxcl  12883  isnzr2  14197  lgscllem  15735  umgr2edg1  16059  eupth2lem1  16308  bdne  16448  apdifflemr  16651