Definition df-ne 2401

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

This definition is referenced by:  neii  2402  neir  2403  nner  2404  nnedc  2405  dcned  2406  neqned  2407  neirr  2409  eqneqall  2410  dcne  2411  nonconne  2412  neeq1  2413  neeq2  2414  neneqd  2421  necon3abii  2436  necon3bii  2438  necon3abid  2439  necon3bid  2441  necon3ad  2442  necon3bd  2443  necon3d  2444  necon3ai  2449  necon3bi  2450  necon1aidc  2451  necon1bidc  2452  necon1idc  2453  necon2ai  2454  necon2ad  2457  necon2bd  2458  necon2d  2459  necon1abiidc  2460  necon1bbiidc  2461  necon1abiddc  2462  necon1bbiddc  2463  necon4aidc  2468  necon4idc  2469  necon4addc  2470  necon4bddc  2471  necon4ddc  2472  necon4abiddc  2473  necon4biddc  2475  necon1addc  2476  necon1bddc  2477  necon1ddc  2478  neanior  2487  ne3anior  2488  nemtbir  2489  nfne  2493  nfned  2494  sbcne12g  3143  dfdif3  3315  ifnefalse  3614  opthpr  3853  prneimg  3855  exmid1dc  4288  exmid1stab  4296  onsucelsucexmid  4626  nnsuc  4712  ftpg  5833  fiintim  7116  updjudhf  7269  netap  7463  elni2  7524  indpi  7552  nngt1ne1  9168  zapne  9544  prime  9569  elnn1uz2  9831  xrnemnf  10002  xrnepnf  10003  xaddcom  10086  xnegdi  10093  xpncan  10096  xleadd1a  10098  xsubge0  10106  flqeqceilz  10570  ndvdssub  12481  gcdsupex  12518  gcdsupcl  12519  gcdeq0  12538  gcd0id  12540  gcdmultiplez  12582  dvdssq  12592  algcvgblem  12611  lcmdvds  12641  lcmid  12642  mulgcddvds  12656  cncongr2  12666  isprm3  12680  isprm4  12681  sqrt2irr  12724  pcxcl  12874  isnzr2  14188  lgscllem  15726  umgr2edg1  16048  bdne  16384  apdifflemr  16587