Definition df-ne 2942

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

This definition is referenced by:  neii  2943  neir  2944  nne  2945  neneqd  2946  neqned  2948  eqneqall  2952  necon2bd  2957  necon1bd  2959  necon3d  2962  necon2d  2964  necon1bi  2970  necon1i  2975  necon3abid  2978  necon1bbid  2981  necon3bid  2986  necon3abii  2988  necon3bii  2994  neor  3035  neanior  3036  neorian  3038  nfne  3044  nfned  3045  nabbib  3046  nelb  3232  nelbOLD  3233  dfpss2  4085  dfdif3  4114  n0f  4342  n0  4346  abn0  4380  2nreu  4441  raaan2  4524  ifnefalse  4540  snnzb  4722  raldifsni  4798  eqsn  4832  n0snor2el  4834  opthpr  4852  opthprneg  4865  unissint  4976  iununi  5102  disji2  5130  opthneg  5481  otthne  5486  opab0  5554  xpcan  6173  xpcan2  6174  xpima  6179  unixpid  6281  unizlim  6485  dff14a  7266  orduniorsuc  7815  dflim3  7833  tfindsg  7847  nn0suc  7883  findsg  7887  xpord2pred  8128  xpord2indlem  8130  frxp3  8134  suppvalbr  8147  frrlem14  8281  wfrlem16OLD  8321  tz7.49  8442  oevn0  8512  fsetexb  8855  php  9207  phpOLD  9219  1sdom  9245  1sdomOLD  9246  fimaxg  9287  fiint  9321  wemapsolem  9542  card2on  9546  brwdomn0  9561  rankxplim2  9872  rankxplim3  9873  updjudhf  9923  carden2a  9958  enpr2  9994  dfackm  10158  fin1a2lem12  10403  ac6num  10471  zorn2lem4  10491  zorn2lem7  10494  brdom3  10520  iundom2g  10532  r1tskina  10774  1re  11211  ltlen  11312  uzm1  12857  xrnemnf  13094  xrnepnf  13095  ioo0  13346  ico0  13367  ioc0  13368  icc0  13369  elfznelfzo  13734  elfznelfzob  13735  injresinjlem  13749  fleqceilz  13816  fsuppmapnn0fiubex  13954  sq01  14185  hash1snb  14376  hashgt12el  14379  hashgt12el2  14380  hashfun  14394  hash2prde  14428  hashge2el2dif  14438  fundmge2nop0  14450  repswcshw  14759  cshw1  14769  incexc2  15781  sqrt2irr  16189  divalglem8  16340  ndvdssub  16349  algcvgblem  16511  lcmcllem  16530  lcmfunsnlem2  16574  isprm3  16617  isprm4  16618  2mulprm  16627  ramcl2lem  16939  cshwshashlem1  17026  cshwshash  17035  smndex2dnrinv  18793  sgrp2nmndlem3  18803  sgrp2nmndlem5  18807  symg2bas  19255  odfval  19395  dprdfeq0  19887  isnirred  20227  isirred2  20228  isnzr2  20290  drngmul0or  20337  drngmuleq0  20339  sdrgacs  20410  lvecvs0or  20714  lvecvscan  20717  isdomn2  20908  isdomn5  20910  domnchr  21076  gsummoncoe1  21820  dmatmul  21991  mulmarep1gsum2  22068  mdetunilem8  22113  mp2pm2mplem4  22303  fvmptnn04if  22343  elcls  22569  opnnei  22616  ist0-3  22841  ist1-2  22843  dfconn2  22915  cnconn  22918  pthaus  23134  xkohaus  23149  hausflim  23477  cldsubg  23607  bcth  24838  ioorinv  25085  tdeglem4  25569  tdeglem4OLD  25570  fta1b  25679  plydivex  25802  aalioulem3  25839  dvradcnv  25925  cxpcl  26174  recxpcl  26175  logrec  26258  isosctrlem2  26314  efrlim  26464  muval2  26628  musum  26685  dchrelbas2  26730  dchrelbas4  26736  dchrfi  26748  dchrptlem3  26759  dchrsum2  26761  sumdchr2  26763  lgscllem  26797  2sqb  26925  2sqcoprm  26928  dchrvmasumiflem2  26995  rpvmasum2  27005  padicabv  27123  padicabvf  27124  padicabvcxp  27125  sltval2  27149  sltres  27155  noseponlem  27157  nosepon  27158  nosepeq  27178  nosupbnd2lem1  27208  noinfbnd2lem1  27223  noetasuplem4  27229  noetainflem4  27233  tglowdim1i  27742  tgbtwnconn1  27816  colline  27890  colmid  27929  lmimid  28035  lmiisolem  28037  brbtwn2  28153  colinearalg  28158  axlowdimlem6  28195  axlowdimlem14  28203  axcontlem12  28223  incistruhgr  28329  umgr2edg1  28458  nb3grprlem1  28627  1egrvtxdg0  28758  vtxdginducedm1lem4  28789  wlkdlem4  28932  lfgriswlk  28935  pthdlem2  29015  wwlksnext  29137  clwwlknclwwlkdif  29222  clwlkclwwlklem2a4  29240  clwwisshclwwsn  29259  1wlkdlem4  29383  eupth2lem1  29461  eupth2lem3lem4  29474  frgr3vlem1  29516  frgr3vlem2  29517  3vfriswmgrlem  29520  4cycl2vnunb  29533  frgrncvvdeqlem8  29549  frgrregorufr  29568  frgrreg  29637  frgrregord013  29638  9p10ne21fool  29714  nvmul0or  29891  nmogtmnf  30011  hvmul0or  30266  hvmulcan  30313  hvmulcan2  30314  hiidge0  30339  bcsiALT  30420  shne0i  30689  nonbooli  30892  nmopgtmnf  31109  unopbd  31256  nmcfnlbi  31293  nmopcoi  31336  chirredi  31635  mdsymlem5  31648  sumdmdlem2  31660  disji2f  31796  aciunf1  31876  fzne1  31987  hashxpe  32007  sitgaddlemb  33336  sgn3da  33529  plymulx  33548  bnj1109  33786  bnj1542  33857  bnj1253  34017  dff15  34076  lfuhgr3  34099  dfacycgr1  34124  subfacp1lem6  34165  cvmsdisj  34250  satffunlem1lem1  34382  satffunlem2lem1  34384  satffun  34389  btwnconn1lem13  35060  lineunray  35108  rankeq1o  35132  elicc3  35191  nn0prpw  35197  ordtoplem  35309  bj-snmoore  35983  irrdifflemf  36195  icorempo  36221  matunitlindflem1  36473  poimirlem1  36478  poimirlem14  36491  poimirlem16  36493  poimirlem19  36496  poimirlem23  36500  poimirlem25  36502  poimirlem26  36503  itg2addnclem3  36530  itgaddnclem2  36536  fdc  36602  ismgmOLD  36707  cvrval2  38133  cvrnbtwn2  38134  cvrnbtwn3  38135  cvlsupr3  38203  cvrat4  38303  2at0mat0  38385  dalawlem13  38743  isltrn2N  38980  trlator0  39031  cdleme22b  39201  dochkrshp  40246  dochkrshp4  40249  lcfl6  40360  lclkrlem2x  40390  metakunt6  40979  metakunt7  40980  metakunt11  40984  metakunt22  40995  nnn1suc  41178  remullid  41303  infdesc  41382  fphpd  41540  jm2.23  41721  isdomn3  41932  dflim6  42000  onsucf1olem  42006  onov0suclim  42010  oenassex  42054  tfsconcatb0  42080  tfsconcat0b  42082  naddwordnexlem4  42138  safesnsupfilb  42155  faosnf0.11b  42164  dfsucon  42260  iunrelexp0  42439  ntrneineine1lem  42821  pm13.196a  43159  onfrALTlem5  43289  onfrALTlem3  43291  en3lpVD  43592  onfrALTlem5VD  43632  onfrALTlem3VD  43634  ax6e2ndeqVD  43656  ax6e2ndeqALT  43678  isosctrlem1ALT  43681  ndisj2  43724  limsupre2lem  44427  cncfiooicclem1  44596  iblcncfioo  44681  stoweidlem28  44731  sge0iunmpt  45121  n0nsn2el  45722  afvfv0bi  45847  2ffzoeq  46023  iccpartiltu  46077  iccpartlt  46079  icceuelpartlem  46090  lighneallem4  46265  oddprmALTV  46342  evenprm2  46369  odd2prm2  46373  even3prm2  46374  upgrwlkupwlk  46505  copisnmnd  46566  pgrpgt2nabl  46996  islindeps  47088  lincext1  47089  lindslinindsimp2lem5  47097  snlindsntor  47106  ldepslinc  47144  m1modmmod  47161  rrx2linest  47382  line2ylem  47391  line2xlem  47393