Definition df-ne 2933

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

This definition is referenced by:  neii  2934  neir  2935  nne  2936  neneqd  2937  neqned  2939  eqneqall  2943  necon2bd  2948  necon1bd  2950  necon3d  2953  necon2d  2955  necon1bi  2960  necon1i  2965  necon3abid  2968  necon1bbid  2971  necon3bid  2976  necon3abii  2978  necon3bii  2984  neor  3024  neanior  3025  neorian  3027  nfne  3033  nfned  3034  nabbib  3035  nelb  3218  dfpss2  4063  dfdif3OLD  4093  n0f  4324  n0  4328  abn0  4360  2nreu  4419  raaan2  4496  ifnefalse  4512  snnzb  4694  raldifsni  4771  eqsn  4805  n0snor2el  4809  opthpr  4827  prneimg2  4831  opthprneg  4841  unissint  4948  iununi  5075  disji2  5103  opthneg  5456  otthne  5461  opab0  5529  xpcan  6165  xpcan2  6166  xpima  6171  unixpid  6273  unizlim  6476  dff14a  7262  orduniorsuc  7822  dflim3  7840  tfindsg  7854  nn0suc  7888  findsg  7891  resf1extb  7928  xpord2pred  8142  xpord2indlem  8144  frxp3  8148  suppvalbr  8161  frrlem14  8296  wfrlem16OLD  8336  tz7.49  8457  oevn0  8525  fsetexb  8876  php  9219  phpOLD  9229  1sdom  9254  1sdomOLD  9255  fimaxg  9293  fiint  9336  fiintOLD  9337  wemapsolem  9562  card2on  9566  brwdomn0  9581  rankxplim2  9892  rankxplim3  9893  updjudhf  9943  carden2a  9978  enpr2  10014  dfackm  10179  fin1a2lem12  10423  ac6num  10491  zorn2lem4  10511  zorn2lem7  10514  brdom3  10540  iundom2g  10552  r1tskina  10794  1re  11233  ltlen  11334  uzm1  12888  xrnemnf  13131  xrnepnf  13132  ioo0  13385  ico0  13406  ioc0  13407  icc0  13408  fzne1  13619  elfznelfzo  13786  elfznelfzob  13787  injresinjlem  13801  fleqceilz  13869  fsuppmapnn0fiubex  14008  sq01  14241  hash1snb  14435  hashgt12el  14438  hashgt12el2  14439  hashfun  14453  hash2prde  14486  hashge2el2dif  14496  fundmge2nop0  14518  repswcshw  14828  cshw1  14838  incexc2  15852  sqrt2irr  16265  divalglem8  16417  ndvdssub  16426  algcvgblem  16594  lcmcllem  16613  lcmfunsnlem2  16657  isprm3  16700  isprm4  16701  2mulprm  16710  ramcl2lem  17027  cshwshashlem1  17113  cshwshash  17122  smndex2dnrinv  18891  sgrp2nmndlem3  18901  sgrp2nmndlem5  18905  symg2bas  19372  odfval  19511  dprdfeq0  20003  isnirred  20378  isirred2  20379  isnzr2  20476  isdomn5  20668  isdomn2OLD  20670  isdomn3  20673  drngmul0orOLD  20719  drngmuleq0  20721  sdrgacs  20759  lvecvs0or  21067  lvecvscan  21070  domnchr  21491  gsummoncoe1  22244  dmatmul  22433  mulmarep1gsum2  22510  mdetunilem8  22555  mp2pm2mplem4  22745  fvmptnn04if  22785  elcls  23009  opnnei  23056  ist0-3  23281  ist1-2  23283  dfconn2  23355  cnconn  23358  pthaus  23574  xkohaus  23589  hausflim  23917  cldsubg  24047  bcth  25279  ioorinv  25527  tdeglem4  26015  fta1b  26127  plydivex  26255  aalioulem3  26292  dvradcnv  26380  cxpcl  26633  recxpcl  26634  logrec  26723  isosctrlem2  26779  efrlim  26929  efrlimOLD  26930  muval2  27094  musum  27151  dchrelbas2  27198  dchrelbas4  27204  dchrfi  27216  dchrptlem3  27227  dchrsum2  27229  sumdchr2  27231  lgscllem  27265  2sqb  27393  2sqcoprm  27396  dchrvmasumiflem2  27463  rpvmasum2  27473  padicabv  27591  padicabvf  27592  padicabvcxp  27593  sltval2  27618  sltres  27624  noseponlem  27626  nosepon  27627  nosepeq  27647  nosupbnd2lem1  27677  noinfbnd2lem1  27692  noetasuplem4  27698  noetainflem4  27702  eln0s  28275  dfnns2  28279  tglowdim1i  28426  tgbtwnconn1  28500  colline  28574  colmid  28613  lmimid  28719  lmiisolem  28721  brbtwn2  28830  colinearalg  28835  axlowdimlem6  28872  axlowdimlem14  28880  axcontlem12  28900  incistruhgr  29004  umgr2edg1  29136  nb3grprlem1  29305  1egrvtxdg0  29437  vtxdginducedm1lem4  29468  wlkdlem4  29611  lfgriswlk  29614  pthdlem2  29696  wwlksnext  29821  clwwlknclwwlkdif  29906  clwlkclwwlklem2a4  29924  clwwisshclwwsn  29943  1wlkdlem4  30067  eupth2lem1  30145  eupth2lem3lem4  30158  frgr3vlem1  30200  frgr3vlem2  30201  3vfriswmgrlem  30204  4cycl2vnunb  30217  frgrncvvdeqlem8  30233  frgrregorufr  30252  frgrreg  30321  frgrregord013  30322  9p10ne21fool  30398  nvmul0or  30577  nmogtmnf  30697  hvmul0or  30952  hvmulcan  30999  hvmulcan2  31000  hiidge0  31025  bcsiALT  31106  shne0i  31375  nonbooli  31578  nmopgtmnf  31795  unopbd  31942  nmcfnlbi  31979  nmopcoi  32022  chirredi  32321  mdsymlem5  32334  sumdmdlem2  32346  n0nsnel  32442  disji2f  32504  aciunf1  32587  hashxpe  32732  sgn3da  32759  elrgspnlem2  33184  ply1dg3rt0irred  33541  sitgaddlemb  34326  plymulx  34526  bnj1109  34763  bnj1542  34834  bnj1253  34994  dff15  35061  lfuhgr3  35088  dfacycgr1  35112  subfacp1lem6  35153  cvmsdisj  35238  satffunlem1lem1  35370  satffunlem2lem1  35372  satffun  35377  btwnconn1lem13  36063  lineunray  36111  rankeq1o  36135  elicc3  36281  nn0prpw  36287  ordtoplem  36399  bj-snmoore  37077  irrdifflemf  37289  icorempo  37315  matunitlindflem1  37586  poimirlem1  37591  poimirlem14  37604  poimirlem16  37606  poimirlem19  37609  poimirlem23  37613  poimirlem25  37615  poimirlem26  37616  itg2addnclem3  37643  itgaddnclem2  37649  fdc  37715  ismgmOLD  37820  cvrval2  39238  cvrnbtwn2  39239  cvrnbtwn3  39240  cvlsupr3  39308  cvrat4  39408  2at0mat0  39490  dalawlem13  39848  isltrn2N  40085  trlator0  40136  cdleme22b  40306  dochkrshp  41351  dochkrshp4  41354  lcfl6  41465  lclkrlem2x  41495  hashnexinj  42087  rspcsbnea  42090  aks6d1c5  42098  metakunt6  42169  metakunt7  42170  metakunt11  42174  metakunt22  42185  nnn1suc  42263  expeqidd  42321  remullid  42423  fimgmcyc  42504  infdesc  42613  fphpd  42786  jm2.23  42967  dflim6  43235  onsucf1olem  43241  onov0suclim  43245  oenassex  43289  tfsconcatb0  43315  tfsconcat0b  43317  naddwordnexlem4  43372  safesnsupfilb  43389  faosnf0.11b  43398  dfsucon  43494  iunrelexp0  43673  ntrneineine1lem  44055  pm13.196a  44386  onfrALTlem5  44515  onfrALTlem3  44517  en3lpVD  44817  onfrALTlem5VD  44857  onfrALTlem3VD  44859  ax6e2ndeqVD  44881  ax6e2ndeqALT  44903  isosctrlem1ALT  44906  rext0  44911  dfac5prim  44963  modelac8prim  44965  ndisj2  45023  limsupre2lem  45701  cncfiooicclem1  45870  iblcncfioo  45955  stoweidlem28  46005  sge0iunmpt  46395  n0nsn2el  47002  afvfv0bi  47129  2ffzoeq  47304  iccpartiltu  47384  iccpartlt  47386  icceuelpartlem  47397  lighneallem4  47572  oddprmALTV  47649  evenprm2  47676  odd2prm2  47680  even3prm2  47681  upgrimpthslem2  47869  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  upgrwlkupwlk  48063  copisnmnd  48092  pgrpgt2nabl  48289  islindeps  48377  lincext1  48378  lindslinindsimp2lem5  48386  snlindsntor  48395  ldepslinc  48433  m1modmmod  48449  rrx2linest  48670  line2ylem  48679  line2xlem  48681  oppcmndclem  48940