Definition df-ne 2931

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

This definition is referenced by:  neii  2932  neir  2933  nne  2934  neneqd  2935  neqned  2937  eqneqall  2941  necon2bd  2946  necon1bd  2948  necon3d  2951  necon2d  2953  necon1bi  2958  necon1i  2963  necon3abid  2966  necon1bbid  2969  necon3bid  2974  necon3abii  2976  necon3bii  2982  neor  3022  neanior  3023  neorian  3025  nfne  3031  nfned  3032  nabbib  3033  nelb  3211  dfpss2  4021  dfdif3OLD  4051  n0f  4279  n0  4283  abn0  4315  2nreu  4374  raaan2  4452  ifnefalse  4468  snnzb  4652  raldifsni  4730  eqsn  4762  n0snor2el  4766  opthpr  4784  prneimg2  4788  opthprneg  4798  unissint  4904  iununi  5030  disji2  5058  opthneg  5423  otthne  5428  opab0  5498  xpcan  6129  xpcan2  6130  xpima  6135  unixpid  6237  unizlim  6436  dff14a  7214  orduniorsuc  7770  dflim3  7787  tfindsg  7801  nn0suc  7834  findsg  7837  resf1extb  7874  xpord2pred  8084  xpord2indlem  8086  frxp3  8090  suppvalbr  8103  frrlem14  8238  tz7.49  8373  oevn0  8439  fsetexb  8800  php  9130  1sdom  9154  fimaxg  9186  fiint  9226  wemapsolem  9454  card2on  9458  brwdomn0  9473  rankxplim2  9793  rankxplim3  9794  updjudhf  9844  carden2a  9879  enpr2  9915  dfackm  10078  fin1a2lem12  10322  ac6num  10390  zorn2lem4  10410  zorn2lem7  10413  brdom3  10439  iundom2g  10451  r1tskina  10694  ltlen  11236  uzm1  12811  xrnemnf  13057  xrnepnf  13058  ioo0  13312  ico0  13333  ioc0  13334  icc0  13335  fzne1  13547  elfznelfzo  13717  elfznelfzob  13718  injresinjlem  13734  fleqceilz  13802  fsuppmapnn0fiubex  13943  sq01  14176  hash1snb  14370  hashgt12el  14373  hashgt12el2  14374  hashfun  14388  hash2prde  14421  hashge2el2dif  14431  fundmge2nop0  14453  repswcshw  14763  cshw1  14773  incexc2  15792  sqrt2irr  16205  divalglem8  16358  ndvdssub  16367  algcvgblem  16535  lcmcllem  16554  lcmfunsnlem2  16598  isprm3  16641  isprm4  16642  2mulprm  16651  ramcl2lem  16969  cshwshashlem1  17055  cshwshash  17064  smndex2dnrinv  18875  sgrp2nmndlem3  18885  sgrp2nmndlem5  18889  symg2bas  19357  odfval  19496  dprdfeq0  19988  isnirred  20389  isirred2  20390  isnzr2  20484  isdomn5  20676  isdomn2OLD  20678  isdomn3  20681  drngmul0orOLD  20727  drngmuleq0  20729  sdrgacs  20767  lvecvs0or  21095  lvecvscan  21098  domnchr  21501  gsummoncoe1  22261  dmatmul  22450  mulmarep1gsum2  22527  mdetunilem8  22572  mp2pm2mplem4  22762  fvmptnn04if  22802  elcls  23026  opnnei  23073  ist0-3  23298  ist1-2  23300  dfconn2  23372  cnconn  23375  pthaus  23591  xkohaus  23606  hausflim  23934  cldsubg  24064  bcth  25284  ioorinv  25531  tdeglem4  26013  fta1b  26125  plydivex  26251  aalioulem3  26288  dvradcnv  26374  cxpcl  26626  recxpcl  26627  logrec  26715  isosctrlem2  26771  efrlim  26921  muval2  27085  musum  27142  dchrelbas2  27188  dchrelbas4  27194  dchrfi  27206  dchrptlem3  27217  dchrsum2  27219  sumdchr2  27221  lgscllem  27255  2sqb  27383  2sqcoprm  27386  dchrvmasumiflem2  27453  rpvmasum2  27463  padicabv  27581  padicabvf  27582  padicabvcxp  27583  ltsval2  27608  ltsres  27614  noseponlem  27616  nosepon  27617  nosepeq  27637  nosupbnd2lem1  27667  noinfbnd2lem1  27682  noetasuplem4  27688  noetainflem4  27692  eln0s  28341  dfnns2  28352  bdayfinbndlem1  28447  tglowdim1i  28557  tgbtwnconn1  28631  colline  28705  colmid  28744  lmimid  28850  lmiisolem  28852  brbtwn2  28962  colinearalg  28967  axlowdimlem6  29004  axlowdimlem14  29012  axcontlem12  29032  incistruhgr  29136  umgr2edg1  29268  nb3grprlem1  29437  1egrvtxdg0  29568  vtxdginducedm1lem4  29599  wlkdlem4  29740  lfgriswlk  29743  pthdlem2  29824  wwlksnext  29949  clwwlknclwwlkdif  30037  clwlkclwwlklem2a4  30055  clwwisshclwwsn  30074  1wlkdlem4  30198  eupth2lem1  30276  eupth2lem3lem4  30289  frgr3vlem1  30331  frgr3vlem2  30332  3vfriswmgrlem  30335  4cycl2vnunb  30348  frgrncvvdeqlem8  30364  frgrregorufr  30383  frgrreg  30452  frgrregord013  30453  9p10ne21fool  30529  nvmul0or  30709  nmogtmnf  30829  hvmul0or  31084  hvmulcan  31131  hvmulcan2  31132  hiidge0  31157  bcsiALT  31238  shne0i  31507  nonbooli  31710  nmopgtmnf  31927  unopbd  32074  nmcfnlbi  32111  nmopcoi  32154  chirredi  32453  mdsymlem5  32466  sumdmdlem2  32478  n0nsnel  32573  disji2f  32635  aciunf1  32724  hashxpe  32868  sgn3da  32895  elrgspnlem2  33292  ply1dg3rt0irred  33632  extdgfialglem1  33824  sitgaddlemb  34480  plymulx  34680  bnj1109  34917  bnj1542  34987  bnj1253  35147  dff15  35215  lfuhgr3  35290  dfacycgr1  35314  subfacp1lem6  35355  cvmsdisj  35440  satffunlem1lem1  35572  satffunlem2lem1  35574  satffun  35579  btwnconn1lem13  36269  lineunray  36317  rankeq1o  36341  elicc3  36487  nn0prpw  36493  ordtoplem  36605  bj-snmoore  37413  irrdifflemf  37627  qdiffALT  37630  icorempo  37655  matunitlindflem1  37925  poimirlem1  37930  poimirlem14  37943  poimirlem16  37945  poimirlem19  37948  poimirlem23  37952  poimirlem25  37954  poimirlem26  37955  itg2addnclem3  37982  itgaddnclem2  37988  fdc  38054  ismgmOLD  38159  cvrval2  39708  cvrnbtwn2  39709  cvrnbtwn3  39710  cvlsupr3  39778  cvrat4  39877  2at0mat0  39959  dalawlem13  40317  isltrn2N  40554  trlator0  40605  cdleme22b  40775  dochkrshp  41820  dochkrshp4  41823  lcfl6  41934  lclkrlem2x  41964  hashnexinj  42555  rspcsbnea  42558  aks6d1c5  42566  nnn1suc  42692  expeqidd  42745  remullid  42854  fimgmcyc  42967  infdesc  43064  fphpd  43232  jm2.23  43412  dflim6  43680  onsucf1olem  43686  onov0suclim  43690  oenassex  43734  tfsconcatb0  43760  tfsconcat0b  43762  naddwordnexlem4  43817  safesnsupfilb  43833  faosnf0.11b  43842  dfsucon  43938  iunrelexp0  44117  ntrneineine1lem  44499  pm13.196a  44829  onfrALTlem5  44957  onfrALTlem3  44959  en3lpVD  45259  onfrALTlem5VD  45299  onfrALTlem3VD  45301  ax6e2ndeqVD  45323  ax6e2ndeqALT  45345  isosctrlem1ALT  45348  rext0  45353  dfac5prim  45405  modelac8prim  45407  permac8prim  45429  ndisj2  45470  limsupre2lem  46140  cncfiooicclem1  46309  iblcncfioo  46394  stoweidlem28  46444  sge0iunmpt  46834  chnerlem1  47300  n0nsn2el  47461  afvfv0bi  47588  2ffzoeq  47764  m1modmmod  47800  modm1p1ne  47812  iccpartiltu  47870  iccpartlt  47872  icceuelpartlem  47883  lighneallem4  48061  oddprmALTV  48151  evenprm2  48178  odd2prm2  48182  even3prm2  48183  upgrimpthslem2  48372  gpg5nbgrvtx03starlem1  48532  gpg5nbgrvtx03starlem2  48533  gpg5nbgrvtx03starlem3  48534  gpg5nbgrvtx13starlem1  48535  gpg5nbgrvtx13starlem2  48536  gpg5nbgrvtx13starlem3  48537  pg4cyclnex  48591  gpg5edgnedg  48594  upgrwlkupwlk  48604  copisnmnd  48633  pgrpgt2nabl  48830  islindeps  48917  lincext1  48918  lindslinindsimp2lem5  48926  snlindsntor  48935  ldepslinc  48973  rrx2linest  49206  line2ylem  49215  line2xlem  49217  oppcmndclem  49480