Definition df-ne 2944

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

This definition is referenced by:  neii  2945  neir  2946  nne  2947  neneqd  2948  neqned  2950  eqneqall  2954  necon2bd  2959  necon1bd  2961  necon3d  2964  necon2d  2966  necon1bi  2972  necon1i  2977  necon3abid  2980  necon1bbid  2983  necon3bid  2988  necon3abii  2990  necon3bii  2996  neor  3036  neanior  3037  neorian  3039  nfne  3045  nfned  3046  nabbi  3047  nelb  3195  nelbOLD  3196  dfpss2  4020  dfdif3  4049  n0f  4276  n0  4280  abn0  4314  2nreu  4375  raaan2  4455  ifnefalse  4471  snnzb  4654  raldifsni  4728  eqsn  4762  n0snor2el  4764  opthpr  4782  opthprneg  4795  unissint  4903  iununi  5028  disji2  5056  opthneg  5396  opab0  5467  xpcan  6079  xpcan2  6080  xpima  6085  unixpid  6187  unizlim  6383  dff14a  7143  orduniorsuc  7677  dflim3  7694  tfindsg  7707  nn0suc  7742  findsg  7746  suppvalbr  7981  frrlem14  8115  wfrlem16OLD  8155  tz7.49  8276  oevn0  8345  fsetexb  8652  php  8993  phpOLD  9005  1sdom  9025  fimaxg  9061  fiint  9091  wemapsolem  9309  card2on  9313  brwdomn0  9328  rankxplim2  9638  rankxplim3  9639  updjudhf  9689  carden2a  9724  dfackm  9922  fin1a2lem12  10167  ac6num  10235  zorn2lem4  10255  zorn2lem7  10258  brdom3  10284  iundom2g  10296  r1tskina  10538  1re  10975  ltlen  11076  uzm1  12616  xrnemnf  12853  xrnepnf  12854  ioo0  13104  ico0  13125  ioc0  13126  icc0  13127  elfznelfzo  13492  elfznelfzob  13493  injresinjlem  13507  fleqceilz  13574  fsuppmapnn0fiubex  13712  sq01  13940  hash1snb  14134  hashgt12el  14137  hashgt12el2  14138  hashfun  14152  hash2prde  14184  hashge2el2dif  14194  fundmge2nop0  14206  repswcshw  14525  cshw1  14535  incexc2  15550  sqrt2irr  15958  divalglem8  16109  ndvdssub  16118  algcvgblem  16282  lcmcllem  16301  lcmfunsnlem2  16345  isprm3  16388  isprm4  16389  2mulprm  16398  ramcl2lem  16710  cshwshashlem1  16797  cshwshash  16806  smndex2dnrinv  18554  sgrp2nmndlem3  18564  sgrp2nmndlem5  18568  symg2bas  19000  odfval  19140  dprdfeq0  19625  isnirred  19942  isirred2  19943  drngmul0or  20012  drngmuleq0  20014  sdrgacs  20069  lvecvs0or  20370  lvecvscan  20373  isnzr2  20534  isdomn2  20570  domnchr  20736  gsummoncoe1  21475  dmatmul  21646  mulmarep1gsum2  21723  mdetunilem8  21768  mp2pm2mplem4  21958  fvmptnn04if  21998  elcls  22224  opnnei  22271  ist0-3  22496  ist1-2  22498  dfconn2  22570  cnconn  22573  pthaus  22789  xkohaus  22804  hausflim  23132  cldsubg  23262  bcth  24493  ioorinv  24740  tdeglem4  25224  tdeglem4OLD  25225  fta1b  25334  plydivex  25457  aalioulem3  25494  dvradcnv  25580  cxpcl  25829  recxpcl  25830  logrec  25913  isosctrlem2  25969  efrlim  26119  muval2  26283  musum  26340  dchrelbas2  26385  dchrelbas4  26391  dchrfi  26403  dchrptlem3  26414  dchrsum2  26416  sumdchr2  26418  lgscllem  26452  2sqb  26580  2sqcoprm  26583  dchrvmasumiflem2  26650  rpvmasum2  26660  padicabv  26778  padicabvf  26779  padicabvcxp  26780  tglowdim1i  26862  tgbtwnconn1  26936  colline  27010  colmid  27049  lmimid  27155  lmiisolem  27157  brbtwn2  27273  colinearalg  27278  axlowdimlem6  27315  axlowdimlem14  27323  axcontlem12  27343  incistruhgr  27449  umgr2edg1  27578  nb3grprlem1  27747  1egrvtxdg0  27878  vtxdginducedm1lem4  27909  wlkdlem4  28053  lfgriswlk  28056  pthdlem2  28136  wwlksnext  28258  clwwlknclwwlkdif  28343  clwlkclwwlklem2a4  28361  clwwisshclwwsn  28380  1wlkdlem4  28504  eupth2lem1  28582  eupth2lem3lem4  28595  frgr3vlem1  28637  frgr3vlem2  28638  3vfriswmgrlem  28641  4cycl2vnunb  28654  frgrncvvdeqlem8  28670  frgrregorufr  28689  frgrreg  28758  frgrregord013  28759  9p10ne21fool  28835  nvmul0or  29012  nmogtmnf  29132  hvmul0or  29387  hvmulcan  29434  hvmulcan2  29435  hiidge0  29460  bcsiALT  29541  shne0i  29810  nonbooli  30013  nmopgtmnf  30230  unopbd  30377  nmcfnlbi  30414  nmopcoi  30457  chirredi  30756  mdsymlem5  30769  sumdmdlem2  30781  nelbOLDOLD  30817  disji2f  30916  aciunf1  31000  fzne1  31109  hashxpe  31127  sitgaddlemb  32315  sgn3da  32508  plymulx  32527  bnj1109  32766  bnj1542  32837  bnj1253  32997  dff15  33056  lfuhgr3  33081  dfacycgr1  33106  subfacp1lem6  33147  cvmsdisj  33232  satffunlem1lem1  33364  satffunlem2lem1  33366  satffun  33371  xpord2pred  33792  xpord2ind  33794  poxp3  33796  frxp3  33797  xpord3pred  33798  sltval2  33859  sltres  33865  noseponlem  33867  nosepon  33868  nosepeq  33888  nosupbnd2lem1  33918  noinfbnd2lem1  33933  noetasuplem4  33939  noetainflem4  33943  btwnconn1lem13  34401  lineunray  34449  rankeq1o  34473  elicc3  34506  nn0prpw  34512  ordtoplem  34624  bj-snmoore  35284  irrdifflemf  35496  icorempo  35522  matunitlindflem1  35773  poimirlem1  35778  poimirlem14  35791  poimirlem16  35793  poimirlem19  35796  poimirlem23  35800  poimirlem25  35802  poimirlem26  35803  itg2addnclem3  35830  itgaddnclem2  35836  fdc  35903  ismgmOLD  36008  cvrval2  37288  cvrnbtwn2  37289  cvrnbtwn3  37290  cvlsupr3  37358  cvrat4  37457  2at0mat0  37539  dalawlem13  37897  isltrn2N  38134  trlator0  38185  cdleme22b  38355  dochkrshp  39400  dochkrshp4  39403  lcfl6  39514  lclkrlem2x  39544  metakunt6  40130  metakunt7  40131  metakunt11  40135  metakunt22  40146  isdomn5  40171  nnn1suc  40296  sn-00id  40384  remulid2  40415  infdesc  40480  fphpd  40638  jm2.23  40818  isdomn3  41029  dfsucon  41130  iunrelexp0  41310  ntrneineine1lem  41694  pm13.196a  42032  onfrALTlem5  42162  onfrALTlem3  42164  en3lpVD  42465  onfrALTlem5VD  42505  onfrALTlem3VD  42507  ax6e2ndeqVD  42529  ax6e2ndeqALT  42551  isosctrlem1ALT  42554  ndisj2  42599  limsupre2lem  43265  cncfiooicclem1  43434  iblcncfioo  43519  stoweidlem28  43569  sge0iunmpt  43956  afvfv0bi  44644  2ffzoeq  44820  iccpartiltu  44874  iccpartlt  44876  icceuelpartlem  44887  lighneallem4  45062  oddprmALTV  45139  evenprm2  45166  odd2prm2  45170  even3prm2  45171  upgrwlkupwlk  45302  copisnmnd  45363  pgrpgt2nabl  45702  islindeps  45794  lincext1  45795  lindslinindsimp2lem5  45803  snlindsntor  45812  ldepslinc  45850  m1modmmod  45867  rrx2linest  46088  line2ylem  46097  line2xlem  46099