Definition df-ne 2378

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

This definition is referenced by:  neii  2379  neir  2380  nner  2381  nnedc  2382  dcned  2383  neqned  2384  neirr  2386  eqneqall  2387  dcne  2388  nonconne  2389  neeq1  2390  neeq2  2391  neneqd  2398  necon3abii  2413  necon3bii  2415  necon3abid  2416  necon3bid  2418  necon3ad  2419  necon3bd  2420  necon3d  2421  necon3ai  2426  necon3bi  2427  necon1aidc  2428  necon1bidc  2429  necon1idc  2430  necon2ai  2431  necon2ad  2434  necon2bd  2435  necon2d  2436  necon1abiidc  2437  necon1bbiidc  2438  necon1abiddc  2439  necon1bbiddc  2440  necon4aidc  2445  necon4idc  2446  necon4addc  2447  necon4bddc  2448  necon4ddc  2449  necon4abiddc  2450  necon4biddc  2452  necon1addc  2453  necon1bddc  2454  necon1ddc  2455  neanior  2464  ne3anior  2465  nemtbir  2466  nfne  2470  nfned  2471  sbcne12g  3115  dfdif3  3287  ifnefalse  3586  opthpr  3819  prneimg  3821  exmid1dc  4252  exmid1stab  4260  onsucelsucexmid  4586  nnsuc  4672  ftpg  5781  fiintim  7043  updjudhf  7196  netap  7386  elni2  7447  indpi  7475  nngt1ne1  9091  zapne  9467  prime  9492  elnn1uz2  9748  xrnemnf  9919  xrnepnf  9920  xaddcom  10003  xnegdi  10010  xpncan  10013  xleadd1a  10015  xsubge0  10023  flqeqceilz  10485  ndvdssub  12316  gcdsupex  12353  gcdsupcl  12354  gcdeq0  12373  gcd0id  12375  gcdmultiplez  12417  dvdssq  12427  algcvgblem  12446  lcmdvds  12476  lcmid  12477  mulgcddvds  12491  cncongr2  12501  isprm3  12515  isprm4  12516  sqrt2irr  12559  pcxcl  12709  isnzr2  14021  lgscllem  15559  bdne  15927  apdifflemr  16127