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 3017
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 3016 . 2 wff 𝐴𝐵
41, 2wceq 1528 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 207 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neii  3018  neir  3019  nne  3020  neneqd  3021  neqned  3023  eqneqall  3027  necon2bd  3032  necon1bd  3034  necon3d  3037  necon2d  3039  necon1bi  3044  necon1i  3049  necon3abid  3052  necon1bbid  3055  necon3bid  3060  necon3abii  3062  necon3bii  3068  neor  3108  neanior  3109  neorian  3111  nfne  3119  nfned  3120  nabbi  3121  nelb  3268  dfpss2  4061  dfdif3  4090  n0f  4306  2nreu  4391  raaan2  4462  ifnefalse  4477  snnzb  4648  raldifsni  4722  eqsn  4756  n0snor2el  4758  opthpr  4776  opthprneg  4789  unissint  4893  iununi  5013  disji2  5040  opthneg  5365  opab0  5433  xpcan  6027  xpcan2  6028  xpima  6033  unixpid  6129  unizlim  6301  dff14a  7019  orduniorsuc  7533  dflim3  7550  tfindsg  7563  nn0suc  7594  findsg  7597  suppvalbr  7825  wfrlem16  7961  tz7.49  8072  oevn0  8131  php  8690  1sdom  8710  fimaxg  8754  fiint  8784  wemapsolem  9003  card2on  9007  brwdomn0  9022  rankxplim2  9298  rankxplim3  9299  updjudhf  9349  carden2a  9384  dfackm  9581  fin1a2lem12  9822  ac6num  9890  zorn2lem4  9910  zorn2lem7  9913  brdom3  9939  iundom2g  9951  r1tskina  10193  1re  10630  ltlen  10730  uzm1  12265  xrnemnf  12502  xrnepnf  12503  ioo0  12753  ico0  12774  ioc0  12775  icc0  12776  elfznelfzo  13132  elfznelfzob  13133  injresinjlem  13147  fleqceilz  13212  fsuppmapnn0fiubex  13350  sq01  13576  hash1snb  13770  hashgt12el  13773  hashgt12el2  13774  hashfun  13788  hash2prde  13818  hashge2el2dif  13828  fundmge2nop0  13840  repswcshw  14164  cshw1  14174  incexc2  15183  sqrt2irr  15592  divalglem8  15741  ndvdssub  15750  algcvgblem  15911  lcmcllem  15930  lcmfunsnlem2  15974  isprm3  16017  isprm4  16018  2mulprm  16027  ramcl2lem  16335  cshwshashlem1  16419  cshwshash  16428  sgrp2nmndlem3  18030  sgrp2nmndlem5  18034  symg2bas  18457  odfval  18591  dprdfeq0  19075  isnirred  19381  isirred2  19382  drngmul0or  19454  drngmuleq0  19456  sdrgacs  19511  lvecvs0or  19811  lvecvscan  19814  isnzr2  19966  isdomn2  20002  gsummoncoe1  20402  domnchr  20609  dmatmul  21036  mulmarep1gsum2  21113  mdetunilem8  21158  mp2pm2mplem4  21347  fvmptnn04if  21387  elcls  21611  opnnei  21658  ist0-3  21883  ist1-2  21885  dfconn2  21957  cnconn  21960  pthaus  22176  xkohaus  22191  hausflim  22519  cldsubg  22648  bcth  23861  ioorinv  24106  tdeglem4  24583  fta1b  24692  plydivex  24815  aalioulem3  24852  dvradcnv  24938  cxpcl  25184  recxpcl  25185  logrec  25268  isosctrlem2  25324  efrlim  25475  muval2  25639  musum  25696  dchrelbas2  25741  dchrelbas4  25747  dchrfi  25759  dchrptlem3  25770  dchrsum2  25772  sumdchr2  25774  lgscllem  25808  2sqb  25936  2sqcoprm  25939  dchrvmasumiflem2  26006  rpvmasum2  26016  padicabv  26134  padicabvf  26135  padicabvcxp  26136  tglowdim1i  26215  tgbtwnconn1  26289  colline  26363  colmid  26402  lmimid  26508  lmiisolem  26510  brbtwn2  26619  colinearalg  26624  axlowdimlem6  26661  axlowdimlem14  26669  axcontlem12  26689  incistruhgr  26792  umgr2edg1  26921  nb3grprlem1  27090  1egrvtxdg0  27221  vtxdginducedm1lem4  27252  wlkdlem4  27395  lfgriswlk  27398  pthdlem2  27477  wwlksnext  27599  clwwlknclwwlkdif  27685  clwlkclwwlklem2a4  27703  clwwisshclwwsn  27722  1wlkdlem4  27847  eupth2lem1  27925  eupth2lem3lem4  27938  frgr3vlem1  27980  frgr3vlem2  27981  3vfriswmgrlem  27984  4cycl2vnunb  27997  frgrncvvdeqlem8  28013  frgrregorufr  28032  frgrreg  28101  frgrregord013  28102  9p10ne21fool  28178  nvmul0or  28355  nmogtmnf  28475  hvmul0or  28730  hvmulcan  28777  hvmulcan2  28778  hiidge0  28803  bcsiALT  28884  shne0i  29153  nonbooli  29356  nmopgtmnf  29573  unopbd  29720  nmcfnlbi  29757  nmopcoi  29800  chirredi  30099  mdsymlem5  30112  sumdmdlem2  30124  nelbOLD  30160  disji2f  30256  aciunf1  30337  fzne1  30438  hashxpe  30456  sitgaddlemb  31506  sgn3da  31699  plymulx  31718  bnj1109  31958  bnj1542  32029  bnj1253  32187  dff15  32251  lfuhgr3  32264  dfacycgr1  32289  subfacp1lem6  32330  cvmsdisj  32415  satffunlem1lem1  32547  satffunlem2lem1  32549  satffun  32554  frrlem14  33034  sltval2  33061  sltres  33067  noseponlem  33069  nosepon  33070  nosepeq  33087  nosupbnd2lem1  33113  noetalem3  33117  btwnconn1lem13  33458  lineunray  33506  rankeq1o  33530  elicc3  33563  nn0prpw  33569  ordtoplem  33681  bj-snmoore  34300  icorempo  34515  matunitlindflem1  34770  poimirlem1  34775  poimirlem14  34788  poimirlem16  34790  poimirlem19  34793  poimirlem23  34797  poimirlem25  34799  poimirlem26  34800  itg2addnclem3  34827  itgaddnclem2  34833  fdc  34903  ismgmOLD  35011  cvrval2  36292  cvrnbtwn2  36293  cvrnbtwn3  36294  cvlsupr3  36362  cvrat4  36461  2at0mat0  36543  dalawlem13  36901  isltrn2N  37138  trlator0  37189  cdleme22b  37359  dochkrshp  38404  dochkrshp4  38407  lcfl6  38518  lclkrlem2x  38548  nnn1suc  39039  sn-00id  39111  remulid2  39129  fphpd  39293  jm2.23  39473  isdomn3  39684  dfsucon  39769  iunrelexp0  39927  ntrneineine1lem  40314  pm13.196a  40626  onfrALTlem5  40756  onfrALTlem3  40758  en3lpVD  41059  onfrALTlem5VD  41099  onfrALTlem3VD  41101  ax6e2ndeqVD  41123  ax6e2ndeqALT  41145  isosctrlem1ALT  41148  ndisj2  41193  limsupre2lem  41885  cncfiooicclem1  42056  iblcncfioo  42143  stoweidlem28  42194  sge0iunmpt  42581  afvfv0bi  43232  2ffzoeq  43409  iccpartiltu  43429  iccpartlt  43431  icceuelpartlem  43442  lighneallem4  43622  oddprmALTV  43699  evenprm2  43726  odd2prm2  43730  even3prm2  43731  upgrwlkupwlk  43862  copisnmnd  43923  smndex2dnrinv  43985  pgrpgt2nabl  44312  islindeps  44406  lincext1  44407  lindslinindsimp2lem5  44415  snlindsntor  44424  ldepslinc  44462  m1modmmod  44479  rrx2linest  44627  line2ylem  44636  line2xlem  44638
  Copyright terms: Public domain W3C validator