Definition df-ne 2958

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 2957	. 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  2959  neir  2960  nne  2961  neneqd  2962  neqned  2964  eqneqall  2968  necon2bd  2973  necon1bd  2975  necon3d  2978  necon2d  2980  necon1bi  2985  necon1i  2990  necon3abid  2993  necon1bbid  2996  necon3bid  3001  necon3abii  3003  necon3bii  3009  neor  3049  neanior  3050  neorian  3052  nfne  3060  nfned  3061  nabbib  3062  nelb  3240  dfpss2  4039  n0f  4299  n0  4303  abn0  4337  2nreu  4405  raaan2  4481  ifnefalse  4497  snnzb  4682  raldifsni  4761  eqsn  4793  n0snor2el  4796  opthpr  4814  prneimg2  4818  opthprneg  4828  unissint  4935  iununi  5063  disji2  5091  opthneg  5461  otthne  5466  opab0  5537  xpcan  6173  xpcan2  6174  xpima  6179  unixpid  6286  unizlim  6486  fvtp0  7202  dff14a  7270  dff15  7272  orduniorsuc  7829  dflim3  7846  tfindsg  7860  nn0suc  7894  findsg  7897  resf1extb  7934  xpord2pred  8146  xpord2indlem  8148  frxp3  8152  suppvalbr  8165  frrlem14  8301  tz7.49  8437  oevn0  8505  fsetexb  8868  php  9204  1sdom  9228  fimaxg  9260  fiint  9299  wemapsolem  9525  card2on  9529  brwdomn0  9544  rankxplim2  9865  rankxplim3  9866  updjudhf  9939  carden2a  9974  enpr2  10010  dfackm  10172  fin1a2lem12  10416  ac6num  10484  zorn2lem4  10504  zorn2lem7  10507  brdom3  10534  iundom2g  10551  r1tskina  10794  ltlen  11338  uzm1  12924  xrnemnf  13170  xrnepnf  13171  ioo0  13425  ico0  13446  ioc0  13447  icc0  13448  fzne1  13661  elfznelfzo  13831  elfznelfzob  13832  injresinjlem  13848  fleqceilz  13917  fsuppmapnn0fiubex  14058  sq01  14291  hash1snb  14486  hashgt12el  14489  hashgt12el2  14490  hashfun  14504  hash2prde  14537  hashge2el2dif  14547  fundmge2nop0  14569  repswcshw  14885  cshw1  14895  sgn3da  15176  incexc2  15929  sqrt2irr  16341  divalglem8  16494  ndvdssub  16503  algcvgblem  16671  lcmcllem  16690  lcmfunsnlem2  16734  isprm3  16777  isprm4  16778  2mulprm  16787  ramcl2lem  17105  cshwshashlem1  17191  cshwshash  17200  smndex2dnrinv  19028  sgrp2nmndlem3  19038  sgrp2nmndlem5  19042  symg2bas  19521  odfval  19660  dprdfeq0  20152  isnirred  20562  isirred2  20563  isnzr2  20679  isdomn5  20873  isdomn3  20877  drngmuleq0  20930  sdrgacs  20968  lvecvs0or  21296  lvecvscan  21299  domnchr  21746  gsummoncoe1  22534  dmatmul  22720  mulmarep1gsum2  22797  mdetunilem8  22842  matunitlindflem1  22902  mp2pm2mplem4  23035  fvmptnn04if  23075  elcls  23299  opnnei  23346  ist0-3  23571  ist1-2  23573  dfconn2  23645  cnconn  23648  pthaus  23865  xkohaus  23880  hausflim  24208  cldsubg  24338  bcth  25558  ioorinv  25805  tdeglem4  26287  fta1b  26399  plymulidp  26513  plydivex  26528  aalioulem3  26567  dvradcnv  26654  cxpcl  26909  recxpcl  26910  logrec  26998  isosctrlem2  27054  efrlim  27204  muval2  27368  musum  27425  dchrelbas2  27471  dchrelbas4  27477  dchrfi  27489  dchrptlem3  27500  dchrsum2  27502  sumdchr2  27504  lgscllem  27538  2sqb  27666  2sqcoprm  27669  dchrvmasumiflem2  27736  rpvmasum2  27746  padicabv  27864  padicabvf  27865  padicabvcxp  27866  ltsval2  27890  ltsres  27896  noseponlem  27898  nosepon  27899  nosepeq  27919  nosupbnd2lem1  27949  noinfbnd2lem1  27964  noetasuplem4  27970  noetainflem4  27974  eln0s  28624  dfnns2  28635  bdayfinbndlem1  28730  tglowdim1i  28841  tgbtwnconn1  28915  colline  28995  colmid  29037  lmimid  29176  lmiisolem  29178  brbtwn2  29348  colinearalg  29353  axlowdimlem6  29390  axlowdimlem14  29398  axcontlem12  29418  incistruhgr  29522  lfuhgr3  29593  umgr2edg1  29657  nb3grprlem1  29826  1egrvtxdg0  29957  vtxdginducedm1lem4  29988  wlkdlem4  30129  lfgriswlk  30136  pthdlem2  30219  wwlksnext  30347  clwwlknclwwlkdif  30435  clwlkclwwlklem2a4  30453  clwwisshclwwsn  30472  1wlkdlem4  30596  dfacycgr1  30615  eupth2lem1  30684  eupth2lem3lem4  30697  frgr3vlem1  30739  frgr3vlem2  30740  3vfriswmgrlem  30743  4cycl2vnunb  30756  frgrncvvdeqlem8  30772  frgrregorufr  30791  frgrreg  30860  frgrregord013  30861  9p10ne21fool  30937  nvmul0or  31117  nmogtmnf  31237  hvmul0or  31492  hvmulcan  31539  hvmulcan2  31540  hiidge0  31565  bcsiALT  31646  shne0i  31915  nonbooli  32118  nmopgtmnf  32335  unopbd  32482  nmcfnlbi  32519  nmopcoi  32562  chirredi  32861  mdsymlem5  32874  sumdmdlem2  32886  n0nsnel  32976  disji2f  33037  aciunf1  33123  hashxpe  33265  elrgspnlem2  33670  ply1dg3rt0irred  33981  extdgfialglem1  34189  sitgaddlemb  34846  bnj1109  35283  bnj1542  35353  bnj1253  35513  subfacp1lem6  35751  cvmsdisj  35836  satffunlem1lem1  35968  satffunlem2lem1  35970  satffun  35975  btwnconn1lem13  36666  lineunray  36714  rankeq1o  36738  nmulel1  36782  elicc3  36923  nn0prpw  36929  ordtoplem  37041  bj-snmoore  37850  irrdifflemf  38064  qdiffALT  38067  icorempo  38092  poimirlem1  38357  poimirlem14  38370  poimirlem16  38372  poimirlem19  38375  poimirlem23  38379  poimirlem25  38381  poimirlem26  38382  itg2addnclem3  38409  itgaddnclem2  38415  fdc  38482  ismgmOLD  38587  cvrval2  40134  cvrnbtwn2  40135  cvrnbtwn3  40136  cvlsupr3  40204  cvrat4  40303  2at0mat0  40385  dalawlem13  40743  isltrn2N  40980  trlator0  41031  cdleme22b  41201  dochkrshp  42246  dochkrshp4  42249  lcfl6  42360  lclkrlem2x  42390  hashnexinj  42981  rspcsbnea  42984  aks6d1c5  42992  nnn1suc  43134  expeqidd  43187  remullid  43296  fimgmcyc  43403  infdesc  43476  fphpd  43644  jm2.23  43824  dflim6  44092  onsucf1olem  44098  onov0suclim  44102  oenassex  44146  tfsconcatb0  44172  tfsconcat0b  44174  naddwordnexlem4  44229  safesnsupfilb  44245  faosnf0.11b  44254  dfsucon  44350  iunrelexp0  44529  ntrneineine1lem  44911  pm13.196a  45225  onfrALTlem5  45352  onfrALTlem3  45354  en3lpVD  45654  onfrALTlem5VD  45694  onfrALTlem3VD  45696  ax6e2ndeqVD  45718  ax6e2ndeqALT  45740  isosctrlem1ALT  45743  rext0  45748  dfac5prim  45800  modelac8prim  45802  permac8prim  45824  ndisj2  45872  limsupre2lem  46539  cncfiooicclem1  46708  iblcncfioo  46793  stoweidlem28  46843  sge0iunmpt  47233  chnerlem1  47697  n0nsn2el  47900  afvfv0bi  48027  2ffzoeq  48203  m1modmmod  48239  modm1p1ne  48251  iccpartiltu  48309  iccpartlt  48311  icceuelpartlem  48322  lighneallem4  48500  oddprmALTV  48590  evenprm2  48617  odd2prm2  48621  even3prm2  48622  upgrimpthslem2  48811  gpg5nbgrvtx03starlem1  48971  gpg5nbgrvtx03starlem2  48972  gpg5nbgrvtx03starlem3  48973  gpg5nbgrvtx13starlem1  48974  gpg5nbgrvtx13starlem2  48975  gpg5nbgrvtx13starlem3  48976  pg4cyclnex  49030  gpg5edgnedg  49033  upgrwlkupwlk  49043  copisnmnd  49071  pgrpgt2nabl  49283  islindeps  49370  lincext1  49371  lindslinindsimp2lem5  49379  snlindsntor  49388  ldepslinc  49426  rrx2linest  49659  line2ylem  49668  line2xlem  49670  oppcmndclem  49930