MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ne Structured version   Visualization version   GIF version

Definition df-ne 2824
Description: Define inequality. (Contributed by NM, 26-May-1993.)
Assertion
Ref Expression
df-ne (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)

Detailed syntax breakdown of Definition df-ne
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2wne 2823 . 2 wff 𝐴𝐵
41, 2wceq 1523 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 196 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neii  2825  neir  2826  nne  2827  neneqd  2828  neqned  2830  eqneqall  2834  necon2bd  2839  necon1bd  2841  necon3d  2844  necon2d  2846  necon1bi  2851  necon1i  2856  necon3abid  2859  necon1bbid  2862  necon3bid  2867  necon3abii  2869  necon3bii  2875  neor  2914  neanior  2915  neorian  2917  nfne  2923  nfned  2924  nabbi  2925  dfpss2  3725  n0f  3960  ifnefalse  4131  snnzb  4286  raldifsni  4357  eqsn  4393  eqsnOLD  4394  n0snor2el  4396  opthpr  4415  unissint  4533  iununi  4642  disji2  4668  opthneg  4979  opab0  5036  xpcan  5605  xpcan2  5606  xpima  5611  unixpid  5708  unizlim  5882  2f1fvneq  6557  dff14a  6567  orduniorsuc  7072  dflim3  7089  tfindsg  7102  nn0suc  7132  findsg  7135  suppvalbr  7344  wfrlem16  7475  tz7.49  7585  oevn0  7640  php  8185  1sdom  8204  fimaxg  8248  fiint  8278  wemapsolem  8496  card2on  8500  brwdomn0  8515  domwdom  8520  rankxplim2  8781  rankxplim3  8782  carden2a  8830  dfackm  9026  fin23lem14  9193  fin1a2lem12  9271  axcc2lem  9296  ac6num  9339  zorn2lem4  9359  zorn2lem7  9362  brdom3  9388  iundom2g  9400  r1tskina  9642  1re  10077  ltlen  10176  uzm1  11756  xrnemnf  11989  xrnepnf  11990  ioo0  12238  ico0  12259  ioc0  12260  icc0  12261  elfznelfzo  12613  elfznelfzob  12614  injresinjlem  12628  fleqceilz  12693  fsuppmapnn0fiubex  12832  sq01  13026  hash1snb  13245  hashgt12el  13248  hashgt12el2  13249  hashfun  13262  hash2prde  13290  hashge2el2dif  13300  fundmge2nop0  13312  ccat1st1st  13448  swrdccatin1  13529  repswcshw  13604  cshw1  13614  xptrrel  13765  incexc2  14614  sqrt2irr  15023  divalglem8  15170  ndvdssub  15180  algcvgblem  15337  lcmcllem  15356  lcmfunsnlem2lem2  15399  lcmfunsnlem2  15400  ncoprmgcdne1b  15410  isprm3  15443  isprm4  15444  ramcl2lem  15760  cshwshashlem1  15849  cshwshash  15858  sgrp2nmndlem3  17459  sgrp2rid2  17460  sgrp2nmndlem5  17463  symg2bas  17864  symgextf  17883  symgextfv  17884  odlem1  18000  gexlem1  18040  dprdfeq0  18467  isnirred  18746  isirred2  18747  drngmul0or  18816  drngmuleq0  18818  lvecvs0or  19156  lvecvscan  19159  isnzr2  19311  isdomn2  19347  cply1mul  19712  gsummoncoe1  19722  domnchr  19928  psgndiflemB  19994  dmatmul  20351  mulmarep1gsum1  20427  mulmarep1gsum2  20428  mdetdiag  20453  mdetunilem8  20473  mdetunilem9  20474  madurid  20498  mp2pm2mplem4  20662  fvmptnn04if  20702  fvmptnn04ifb  20704  elcls  20925  opnnei  20972  ist0-3  21197  ist1-2  21199  dfconn2  21270  cnconn  21273  pthaus  21489  xkohaus  21504  hausflim  21832  cldsubg  21961  bcth  23172  ioorinv  23390  tdeglem4  23865  fta1b  23974  plydivex  24097  plyexmo  24113  aalioulem3  24134  dvradcnv  24220  logtayllem  24450  logtayl  24451  cxpcl  24465  recxpcl  24466  logrec  24546  isosctrlem2  24594  efrlim  24741  muval2  24905  musum  24962  dchrelbas2  25007  dchrelbas4  25013  dchrfi  25025  dchrptlem3  25036  dchrsum2  25038  sumdchr2  25040  lgscllem  25074  2sqb  25202  dchrvmasumiflem2  25236  rpvmasum2  25246  padicabv  25364  padicabvf  25365  padicabvcxp  25366  tglowdim1i  25441  tgbtwnconn1  25515  colline  25589  colmid  25628  lmimid  25731  lmiisolem  25733  brbtwn2  25830  colinearalg  25835  axlowdimlem6  25872  axlowdimlem14  25880  axcontlem12  25900  incistruhgr  26019  umgr2edg1  26148  nb3grprlem1  26326  1egrvtxdg0  26463  vtxdginducedm1lem4  26494  wlkdlem4  26638  lfgriswlk  26641  pthdlem2  26720  wwlksnext  26856  clwwlknclwwlkdif  26945  clwlkclwwlklem2a4  26963  clwwisshclwwsn  26973  1wlkdlem4  27118  eupth2lem1  27196  eupth2lem3lem4  27209  frgr3vlem1  27253  frgr3vlem2  27254  3vfriswmgrlem  27257  4cycl2vnunb  27270  frgrncvvdeqlem8  27286  frgrregorufr  27305  frgrreg  27381  frgrregord013  27382  nvmul0or  27633  nmogtmnf  27753  hvmul0or  28010  hvmulcan  28057  hvmulcan2  28058  hiidge0  28083  bcsiALT  28164  shne0i  28435  nonbooli  28638  nmopgtmnf  28855  unopbd  29002  nmcfnlbi  29039  nmopcoi  29082  chirredi  29381  mdsymlem5  29394  sumdmdlem2  29406  disji2f  29516  imadifxp  29540  aciunf1  29591  2sqcoprm  29775  sitgaddlemb  30538  sgn3da  30731  plymulx  30753  bnj1109  30983  bnj1542  31053  bnj1253  31211  subfacp1lem6  31293  cvmsdisj  31378  sltval2  31934  sltres  31940  noseponlem  31942  nosepon  31943  nosepeq  31960  nosupbnd2lem1  31986  noetalem3  31990  btwnconn1lem13  32331  lineunray  32379  rankeq1o  32403  elicc3  32436  nn0prpw  32443  ordtoplem  32559  bj-ismooredr2  33190  bj-snmoore  33193  icorempt2  33329  matunitlindflem1  33535  poimirlem1  33540  poimirlem14  33553  poimirlem16  33555  poimirlem19  33558  poimirlem23  33562  poimirlem25  33564  poimirlem26  33565  itg2addnclem3  33593  itgaddnclem2  33599  fdc  33671  ismgmOLD  33779  cvrval2  34879  cvrnbtwn2  34880  cvrnbtwn3  34881  cvlsupr3  34949  cvrat4  35047  2at0mat0  35129  dalawlem13  35487  isltrn2N  35724  trlator0  35776  cdleme22b  35946  dochkrshp  36992  dochkrshp4  36995  lcfl6  37106  lclkrlem2x  37136  fphpd  37697  jm2.23  37880  sdrgacs  38088  isdomn3  38099  iunrelexp0  38311  ntrneineine1lem  38699  pm13.196a  38932  onfrALTlem5  39074  onfrALTlem3  39076  en3lpVD  39394  onfrALTlem5VD  39435  onfrALTlem3VD  39437  ax6e2ndeqVD  39459  ax6e2ndeqALT  39481  isosctrlem1ALT  39484  ndisj2  39532  limsupre2lem  40274  cncfiooicclem1  40424  iblcncfioo  40512  stoweidlem28  40563  sge0iunmpt  40953  raaan2  41496  afvfv0bi  41553  2ffzoeq  41663  iccpartiltu  41683  iccpartlt  41685  icceuelpartlem  41696  cshword2  41762  lighneallem4  41852  oddprmALTV  41923  evenprm2  41948  odd2prm2  41952  even3prm2  41953  upgrwlkupwlk  42046  copisnmnd  42134  pgrpgt2nabl  42472  islindeps  42567  lincext1  42568  lindslinindsimp2lem5  42576  snlindsntor  42585  ldepslinc  42623  m1modmmod  42641
  Copyright terms: Public domain W3C validator