Definition df-ne 2341

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

This definition is referenced by:  neii  2342  neir  2343  nner  2344  nnedc  2345  dcned  2346  neqned  2347  neirr  2349  eqneqall  2350  dcne  2351  nonconne  2352  neeq1  2353  neeq2  2354  neneqd  2361  necon3abii  2376  necon3bii  2378  necon3abid  2379  necon3bid  2381  necon3ad  2382  necon3bd  2383  necon3d  2384  necon3ai  2389  necon3bi  2390  necon1aidc  2391  necon1bidc  2392  necon1idc  2393  necon2ai  2394  necon2ad  2397  necon2bd  2398  necon2d  2399  necon1abiidc  2400  necon1bbiidc  2401  necon1abiddc  2402  necon1bbiddc  2403  necon4aidc  2408  necon4idc  2409  necon4addc  2410  necon4bddc  2411  necon4ddc  2412  necon4abiddc  2413  necon4biddc  2415  necon1addc  2416  necon1bddc  2417  necon1ddc  2418  neanior  2427  ne3anior  2428  nemtbir  2429  nfne  2433  nfned  2434  sbcne12g  3067  dfdif3  3237  ifnefalse  3537  opthpr  3759  prneimg  3761  exmid1dc  4186  onsucelsucexmid  4514  nnsuc  4600  ftpg  5680  fiintim  6906  updjudhf  7056  elni2  7276  indpi  7304  nngt1ne1  8913  zapne  9286  prime  9311  elnn1uz2  9566  xrnemnf  9734  xrnepnf  9735  xaddcom  9818  xnegdi  9825  xpncan  9828  xleadd1a  9830  xsubge0  9838  flqeqceilz  10274  ndvdssub  11889  gcdsupex  11912  gcdsupcl  11913  gcdeq0  11932  gcd0id  11934  gcdmultiplez  11976  dvdssq  11986  algcvgblem  12003  lcmdvds  12033  lcmid  12034  mulgcddvds  12048  cncongr2  12058  isprm3  12072  isprm4  12073  sqrt2irr  12116  pcxcl  12265  lgscllem  13702  bdne  13888  exmid1stab  14033  apdifflemr  14079