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 2781
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 2779 . 2 wff 𝐴𝐵
41, 2wceq 1474 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 194 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neii  2783  neir  2784  nne  2785  neneqd  2786  neqned  2788  eqneqall  2792  necon2bd  2797  necon1bd  2799  necon3d  2802  necon2d  2804  necon1bi  2809  necon1i  2814  necon3abid  2817  necon1bbid  2820  necon3bid  2825  necon3abii  2827  necon3bii  2833  neor  2872  neanior  2873  neorian  2875  nfne  2881  nfned  2882  nabbi  2883  dfpss2  3653  n0f  3885  ifnefalse  4047  snnzb  4197  raldifsni  4264  eqsn  4298  eqsnOLD  4299  opthpr  4319  unissint  4430  iununi  4540  disji2  4563  opthneg  4869  xpcan  5474  xpcan2  5475  xpima  5480  unixpid  5572  unizlim  5746  dff14a  6404  mpt2difsnif  6628  orduniorsuc  6899  dflim3  6916  tfindsg  6929  nn0suc  6959  findsg  6962  suppvalbr  7163  wfrlem16  7294  tz7.49  7404  oevn0  7459  php  8006  1sdom  8025  fimaxg  8069  fiint  8099  wemapsolem  8315  card2on  8319  brwdomn0  8334  domwdom  8339  rankxplim2  8603  rankxplim3  8604  carden2a  8652  dfackm  8848  fin23lem14  9015  fin1a2lem12  9093  axcc2lem  9118  ac6num  9161  zorn2lem4  9181  zorn2lem7  9184  brdom3  9208  iundom2g  9218  r1tskina  9460  1re  9895  ltlen  9989  uzm1  11552  xrnemnf  11790  xrnepnf  11791  ioo0  12029  ico0  12050  ioc0  12051  icc0  12052  elfznelfzo  12396  elfznelfzob  12397  injresinjlem  12407  fleqceilz  12472  fsuppmapnn0fiubex  12611  sq01  12805  hash1snb  13022  hashgt12el  13024  hashgt12el2  13025  hashfun  13038  hash2prde  13063  hashge2el2dif  13069  swrdccatin1  13282  repswcshw  13357  cshw1  13367  xptrrel  13515  incexc2  14357  sqrt2irr  14765  divalglem8  14909  ndvdssub  14919  algcvgblem  15076  lcmcllem  15095  lcmfunsnlem2lem2  15138  lcmfunsnlem2  15139  ncoprmgcdne1b  15149  isprm2lem  15180  isprm3  15182  isprm4  15183  ramcl2lem  15499  cshwshashlem1  15588  cshwshash  15597  isnsgrp  17059  isnmnd  17069  sgrp2nmndlem3  17183  sgrp2rid2  17184  sgrp2nmndlem5  17187  symg2bas  17589  symgextf  17608  symgextfv  17609  odlem1  17725  gexlem1  17765  dprdfeq0  18192  isnirred  18471  isirred2  18472  drngmul0or  18539  drngmuleq0  18541  lvecvs0or  18877  lvecvscan  18880  isnzr2  19032  isdomn2  19068  cply1mul  19433  gsummoncoe1  19443  domnchr  19646  psgndiflemB  19712  dmatmul  20069  mulmarep1gsum1  20145  mulmarep1gsum2  20146  mdetdiag  20171  mdetunilem8  20191  mdetunilem9  20192  madurid  20216  mp2pm2mplem4  20380  fvmptnn04if  20420  fvmptnn04ifb  20422  elcls  20634  opnnei  20681  ist0-3  20906  ist1-2  20908  dfcon2  20979  cnconn  20982  pthaus  21198  xkohaus  21213  hausflim  21542  cldsubg  21671  bcth  22878  ioorinv  23094  tdeglem4  23568  fta1b  23677  plydivex  23800  plyexmo  23816  aalioulem3  23837  dvradcnv  23923  logtayllem  24149  logtayl  24150  cxpcl  24164  recxpcl  24165  logrec  24245  isosctrlem2  24293  efrlim  24440  muval2  24604  musum  24661  dchrelbas2  24706  dchrelbas4  24712  dchrfi  24724  dchrptlem3  24735  dchrsum2  24737  sumdchr2  24739  lgscllem  24773  2sqb  24901  dchrvmasumiflem2  24935  rpvmasum2  24945  padicabv  25063  padicabvf  25064  padicabvcxp  25065  tglowdim1i  25140  tgbtwnconn1  25215  colline  25289  colmid  25328  lmimid  25431  lmiisolem  25433  brbtwn2  25530  colinearalg  25535  axlowdimlem6  25572  axlowdimlem14  25580  axcontlem12  25600  usgra2edg1  25705  nbgranself  25756  nb3graprlem1  25773  uvtx01vtx  25813  wlkdvspthlem  25930  usgrcyclnl1  25961  usgrcyclnl2  25962  constr3trllem2  25972  wwlknext  26045  clwlkisclwwlklem2a4  26105  clwwisshclwwn  26129  clwlknclwlkdifs  26280  eupath2lem1  26297  frgra3vlem1  26320  frgra3vlem2  26321  3vfriswmgralem  26324  2pthfrgra  26331  4cycl2vnunb  26337  n4cyclfrgra  26338  frgrancvvdeqlemA  26357  frgrancvvdeqlemB  26358  frgrancvvdeqlemC  26359  frgraregorufr0  26372  frgraregorufr  26373  numclwwlk3lem  26428  frgrareg  26437  frgraregord013  26438  nvmul0or  26682  nmogtmnf  26802  hvmul0or  27059  hvmulcan  27106  hvmulcan2  27107  hiidge0  27132  bcsiALT  27213  shne0i  27484  nonbooli  27687  nmopgtmnf  27904  unopbd  28051  nmcfnlbi  28088  nmopcoi  28131  chirredi  28430  mdsymlem5  28443  sumdmdlem2  28455  disji2f  28565  imadifxp  28589  aciunf1  28638  2sqcoprm  28771  sitgaddlemb  29530  sgn3da  29723  plymulx  29744  bnj1109  29904  bnj1542  29974  bnj1253  30132  subfacp1lem6  30214  cvmsdisj  30299  sltval2  30846  sltres  30854  noseponlem  30858  nosepon  30859  nodenselem4  30876  nodenselem5  30877  nodenselem7  30879  nobndup  30892  nobnddown  30893  nofulllem5  30898  btwnconn1lem13  31169  lineunray  31217  rankeq1o  31241  elicc3  31274  nn0prpw  31281  ordtoplem  31397  icorempt2  32158  matunitlindflem1  32358  poimirlem1  32363  poimirlem14  32376  poimirlem16  32378  poimirlem19  32381  poimirlem23  32385  poimirlem25  32387  poimirlem26  32388  itg2addnclem3  32416  itgaddnclem2  32422  fdc  32494  ismgmOLD  32602  cvrval2  33362  cvrnbtwn2  33363  cvrnbtwn3  33364  cvlsupr3  33432  cvrat4  33530  2at0mat0  33612  dalawlem13  33970  isltrn2N  34207  trlator0  34259  cdleme22b  34430  dochkrshp  35476  dochkrshp4  35479  lcfl6  35590  lclkrlem2x  35620  fphpd  36181  jm2.23  36364  sdrgacs  36573  isdomn3  36584  iunrelexp0  36796  ntrneineine1lem  37185  pm13.196a  37420  onfrALTlem5  37561  onfrALTlem3  37563  en3lpVD  37885  onfrALTlem5VD  37926  onfrALTlem3VD  37928  ax6e2ndeqVD  37950  ax6e2ndeqALT  37972  isosctrlem1ALT  37975  ndisj2  38026  cncfiooicclem1  38562  iblcncfioo  38653  stoweidlem28  38704  sge0iunmpt  39094  raaan2  39607  2reu4a  39621  afvfv0bi  39665  iccpartiltu  39744  iccpartlt  39746  icceuelpartlem  39757  lighneallem4  39849  oddprmALTV  39920  evenprm2  39945  cshword2  40084  pr1eqbg  40097  n0snor2el  40102  2f1fvneq  40117  fundmge2nop0  40131  2ffzoeq  40167  incistruhgr  40286  umgr2edg1  40419  nb3grprlem1  40589  1egrvtxdg0  40708  upgr1wlkwlk  40828  1wlkdlem4  40875  lfgriswlk  40878  pthdlem2  40955  wwlksnext  41080  clwlkclwwlklem2a4  41187  clwwisshclwwsn  41217  11wlkdlem4  41288  eupth2lem1  41367  eupth2lem3lem4  41380  frgr3vlem1  41424  frgr3vlem2  41425  3vfriswmgrlem  41428  4cycl2vnunb-av  41441  frgrncvvdeqlemB  41458  frgrregorufr  41471  av-frgrareg  41529  av-frgraregord013  41530  copisnmnd  41580  fdmdifeqresdif  41894  pgrpgt2nabl  41922  islindeps  42017  lincext1  42018  lindslinindsimp2lem5  42026  snlindsntor  42035  ldepslinc  42073  m1modmmod  42091
  Copyright terms: Public domain W3C validator