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  7338  netap  7533  elni2  7594  indpi  7622  nngt1ne1  9237  zapne  9615  prime  9640  elnn1uz2  9902  xrnemnf  10073  xrnepnf  10074  xaddcom  10157  xnegdi  10164  xpncan  10167  xleadd1a  10169  xsubge0  10177  flqeqceilz  10643  ndvdssub  12571  gcdsupex  12608  gcdsupcl  12609  gcdeq0  12628  gcd0id  12630  gcdmultiplez  12672  dvdssq  12682  algcvgblem  12701  lcmdvds  12731  lcmid  12732  mulgcddvds  12746  cncongr2  12756  isprm3  12770  isprm4  12771  sqrt2irr  12814  pcxcl  12964  isnzr2  14279  lgscllem  15826  umgr2edg1  16150  eupth2lem1  16399  eupth2lem3lem4fi  16414  bdne  16569  apdifflemr  16779