Definition df-ne 2959

Description: Define inequality. (Contributed by NM, 26-May-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 2958	. 2 wff 𝐴 ≠ 𝐵
4	1, 2	wceq 1570	. . 3 wff 𝐴 = 𝐵
5	4	wn 3	. 2 wff ¬ 𝐴 = 𝐵
6	3, 5	wb 209	1 wff (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)

This definition is used by:  neii  2960  neir  2961  nne  2962  neneqd  2963  neqned  2965  eqneqall  2969  necon2bd  2974  necon1bd  2976  necon3d  2979  necon2d  2981  necon1bi  2986  necon1i  2991  necon3abid  2994  necon1bbid  2997  necon3bid  3002  necon3abii  3004  necon3bii  3010  neor  3050  neanior  3051  neorian  3053  nfne  3061  nfned  3062  nabbib  3063  nelb  3241  dfpss2  4042  dfdif3OLD  4073  n0f  4303  n0  4307  abn0  4341  2nreu  4409  raaan2  4483  ifnefalse  4499  snnzb  4684  raldifsni  4763  eqsn  4795  n0snor2el  4798  opthpr  4816  prneimg2  4820  opthprneg  4830  unissint  4937  iununi  5065  disji2  5093  opthneg  5463  otthne  5468  opab0  5539  xpcan  6174  xpcan2  6175  xpima  6180  unixpid  6285  unizlim  6485  dff14a  7268  orduniorsuc  7822  dflim3  7839  tfindsg  7853  nn0suc  7887  findsg  7890  resf1extb  7927  xpord2pred  8137  xpord2indlem  8139  frxp3  8143  suppvalbr  8156  frrlem14  8292  tz7.49  8428  oevn0  8496  fsetexb  8857  php  9187  1sdom  9211  fimaxg  9243  fiint  9282  wemapsolem  9508  card2on  9512  brwdomn0  9527  rankxplim2  9848  rankxplim3  9849  updjudhf  9922  carden2a  9957  enpr2  9993  dfackm  10155  fin1a2lem12  10399  ac6num  10467  zorn2lem4  10487  zorn2lem7  10490  brdom3  10516  iundom2g  10528  r1tskina  10771  ltlen  11315  uzm1  12900  xrnemnf  13146  xrnepnf  13147  ioo0  13401  ico0  13422  ioc0  13423  icc0  13424  fzne1  13637  elfznelfzo  13807  elfznelfzob  13808  injresinjlem  13824  fleqceilz  13892  fsuppmapnn0fiubex  14033  sq01  14266  hash1snb  14461  hashgt12el  14464  hashgt12el2  14465  hashfun  14479  hash2prde  14512  hashge2el2dif  14522  fundmge2nop0  14544  repswcshw  14854  cshw1  14864  sgn3da  15143  incexc2  15897  sqrt2irr  16309  divalglem8  16462  ndvdssub  16471  algcvgblem  16639  lcmcllem  16658  lcmfunsnlem2  16702  isprm3  16745  isprm4  16746  2mulprm  16755  ramcl2lem  17073  cshwshashlem1  17159  cshwshash  17168  smndex2dnrinv  18981  sgrp2nmndlem3  18991  sgrp2nmndlem5  18995  symg2bas  19467  odfval  19606  dprdfeq0  20098  isnirred  20507  isirred2  20508  isnzr2  20624  isdomn5  20818  isdomn3  20822  drngmuleq0  20875  sdrgacs  20913  lvecvs0or  21241  lvecvscan  21244  domnchr  21691  gsummoncoe1  22477  dmatmul  22663  mulmarep1gsum2  22740  mdetunilem8  22785  mp2pm2mplem4  22975  fvmptnn04if  23015  elcls  23239  opnnei  23286  ist0-3  23511  ist1-2  23513  dfconn2  23585  cnconn  23588  pthaus  23804  xkohaus  23819  hausflim  24147  cldsubg  24277  bcth  25497  ioorinv  25744  tdeglem4  26226  fta1b  26338  plymulidp  26452  plydivex  26467  aalioulem3  26506  dvradcnv  26593  cxpcl  26848  recxpcl  26849  logrec  26937  isosctrlem2  26993  efrlim  27143  muval2  27307  musum  27364  dchrelbas2  27410  dchrelbas4  27416  dchrfi  27428  dchrptlem3  27439  dchrsum2  27441  sumdchr2  27443  lgscllem  27477  2sqb  27605  2sqcoprm  27608  dchrvmasumiflem2  27675  rpvmasum2  27685  padicabv  27803  padicabvf  27804  padicabvcxp  27805  ltsval2  27829  ltsres  27835  noseponlem  27837  nosepon  27838  nosepeq  27858  nosupbnd2lem1  27888  noinfbnd2lem1  27903  noetasuplem4  27909  noetainflem4  27913  eln0s  28563  dfnns2  28574  bdayfinbndlem1  28669  tglowdim1i  28779  tgbtwnconn1  28853  colline  28932  colmid  28974  lmimid  29112  lmiisolem  29114  brbtwn2  29264  colinearalg  29269  axlowdimlem6  29306  axlowdimlem14  29314  axcontlem12  29334  incistruhgr  29438  umgr2edg1  29570  nb3grprlem1  29739  1egrvtxdg0  29870  vtxdginducedm1lem4  29901  wlkdlem4  30042  lfgriswlk  30045  pthdlem2  30126  wwlksnext  30251  clwwlknclwwlkdif  30339  clwlkclwwlklem2a4  30357  clwwisshclwwsn  30376  1wlkdlem4  30500  eupth2lem1  30578  eupth2lem3lem4  30591  frgr3vlem1  30633  frgr3vlem2  30634  3vfriswmgrlem  30637  4cycl2vnunb  30650  frgrncvvdeqlem8  30666  frgrregorufr  30685  frgrreg  30754  frgrregord013  30755  9p10ne21fool  30831  nvmul0or  31011  nmogtmnf  31131  hvmul0or  31386  hvmulcan  31433  hvmulcan2  31434  hiidge0  31459  bcsiALT  31540  shne0i  31809  nonbooli  32012  nmopgtmnf  32229  unopbd  32376  nmcfnlbi  32413  nmopcoi  32456  chirredi  32755  mdsymlem5  32768  sumdmdlem2  32780  n0nsnel  32870  disji2f  32931  aciunf1  33017  hashxpe  33161  elrgspnlem2  33572  ply1dg3rt0irred  33883  extdgfialglem1  34091  sitgaddlemb  34747  bnj1109  35184  bnj1542  35254  bnj1253  35414  dff15  35481  lfuhgr3  35620  dfacycgr1  35644  subfacp1lem6  35685  cvmsdisj  35770  satffunlem1lem1  35902  satffunlem2lem1  35904  satffun  35909  btwnconn1lem13  36599  lineunray  36647  rankeq1o  36671  nmulel1  36715  elicc3  36856  nn0prpw  36862  ordtoplem  36974  bj-snmoore  37783  irrdifflemf  37997  qdiffALT  38000  icorempo  38025  matunitlindflem1  38295  poimirlem1  38300  poimirlem14  38313  poimirlem16  38315  poimirlem19  38318  poimirlem23  38322  poimirlem25  38324  poimirlem26  38325  itg2addnclem3  38352  itgaddnclem2  38358  fdc  38424  ismgmOLD  38529  cvrval2  40076  cvrnbtwn2  40077  cvrnbtwn3  40078  cvlsupr3  40146  cvrat4  40245  2at0mat0  40327  dalawlem13  40685  isltrn2N  40922  trlator0  40973  cdleme22b  41143  dochkrshp  42188  dochkrshp4  42191  lcfl6  42302  lclkrlem2x  42332  hashnexinj  42923  rspcsbnea  42926  aks6d1c5  42934  nnn1suc  43061  expeqidd  43114  remullid  43223  fimgmcyc  43330  infdesc  43403  fphpd  43571  jm2.23  43751  dflim6  44019  onsucf1olem  44025  onov0suclim  44029  oenassex  44073  tfsconcatb0  44099  tfsconcat0b  44101  naddwordnexlem4  44156  safesnsupfilb  44172  faosnf0.11b  44181  dfsucon  44277  iunrelexp0  44456  ntrneineine1lem  44838  pm13.196a  45152  onfrALTlem5  45279  onfrALTlem3  45281  en3lpVD  45581  onfrALTlem5VD  45621  onfrALTlem3VD  45623  ax6e2ndeqVD  45645  ax6e2ndeqALT  45667  isosctrlem1ALT  45670  rext0  45675  dfac5prim  45727  modelac8prim  45729  permac8prim  45751  ndisj2  45799  limsupre2lem  46466  cncfiooicclem1  46635  iblcncfioo  46720  stoweidlem28  46770  sge0iunmpt  47160  chnerlem1  47626  n0nsn2el  47790  afvfv0bi  47917  2ffzoeq  48093  m1modmmod  48129  modm1p1ne  48141  iccpartiltu  48199  iccpartlt  48201  icceuelpartlem  48212  lighneallem4  48390  oddprmALTV  48480  evenprm2  48507  odd2prm2  48511  even3prm2  48512  upgrimpthslem2  48701  gpg5nbgrvtx03starlem1  48861  gpg5nbgrvtx03starlem2  48862  gpg5nbgrvtx03starlem3  48863  gpg5nbgrvtx13starlem1  48864  gpg5nbgrvtx13starlem2  48865  gpg5nbgrvtx13starlem3  48866  pg4cyclnex  48920  gpg5edgnedg  48923  upgrwlkupwlk  48933  copisnmnd  48962  pgrpgt2nabl  49174  islindeps  49261  lincext1  49262  lindslinindsimp2lem5  49270  snlindsntor  49279  ldepslinc  49317  rrx2linest  49550  line2ylem  49559  line2xlem  49561  oppcmndclem  49823