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 2925
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 2924 . 2 wff 𝐴𝐵
41, 2wceq 1624 . . 3 wff 𝐴 = 𝐵
54wn 3 . 2 wff ¬ 𝐴 = 𝐵
63, 5wb 196 1 wff (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  neii  2926  neir  2927  nne  2928  neneqd  2929  neqned  2931  eqneqall  2935  necon2bd  2940  necon1bd  2942  necon3d  2945  necon2d  2947  necon1bi  2952  necon1i  2957  necon3abid  2960  necon1bbid  2963  necon3bid  2968  necon3abii  2970  necon3bii  2976  neor  3015  neanior  3016  neorian  3018  nfne  3024  nfned  3025  nabbi  3026  dfpss2  3826  dfdif3  3855  n0f  4062  ifnefalse  4234  snnzb  4390  raldifsni  4462  eqsn  4498  eqsnOLD  4499  n0snor2el  4501  opthpr  4520  opthprneg  4537  unissint  4645  iununi  4754  disji2  4780  opthneg  5090  opab0  5149  xpcan  5720  xpcan2  5721  xpima  5726  unixpid  5823  unizlim  5997  2f1fvneq  6672  dff14a  6682  orduniorsuc  7187  dflim3  7204  tfindsg  7217  nn0suc  7247  findsg  7250  suppvalbr  7459  wfrlem16  7591  tz7.49  7701  oevn0  7756  php  8301  1sdom  8320  fimaxg  8364  fiint  8394  wemapsolem  8612  card2on  8616  brwdomn0  8631  domwdom  8636  rankxplim2  8908  rankxplim3  8909  carden2a  8974  dfackm  9172  fin23lem14  9339  fin1a2lem12  9417  axcc2lem  9442  ac6num  9485  zorn2lem4  9505  zorn2lem7  9508  brdom3  9534  iundom2g  9546  r1tskina  9788  1re  10223  ltlen  10322  uzm1  11903  xrnemnf  12136  xrnepnf  12137  ioo0  12385  ico0  12406  ioc0  12407  icc0  12408  elfznelfzo  12759  elfznelfzob  12760  injresinjlem  12774  fleqceilz  12839  fsuppmapnn0fiubex  12978  sq01  13172  hash1snb  13391  hashgt12el  13394  hashgt12el2  13395  hashfun  13408  hash2prde  13436  hashge2el2dif  13446  fundmge2nop0  13458  ccat1st1st  13594  swrdccatin1  13675  repswcshw  13750  cshw1  13760  xptrrel  13912  incexc2  14761  sqrt2irr  15170  divalglem8  15317  ndvdssub  15327  algcvgblem  15484  lcmcllem  15503  lcmfunsnlem2lem2  15546  lcmfunsnlem2  15547  ncoprmgcdne1b  15557  isprm3  15590  isprm4  15591  ramcl2lem  15907  cshwshashlem1  15996  cshwshash  16005  sgrp2nmndlem3  17605  sgrp2rid2  17606  sgrp2nmndlem5  17609  symg2bas  18010  symgextf  18029  symgextfv  18030  odlem1  18146  gexlem1  18186  dprdfeq0  18613  isnirred  18892  isirred2  18893  drngmul0or  18962  drngmuleq0  18964  lvecvs0or  19302  lvecvscan  19305  isnzr2  19457  isdomn2  19493  cply1mul  19858  gsummoncoe1  19868  domnchr  20074  psgndiflemB  20140  dmatmul  20497  mulmarep1gsum1  20573  mulmarep1gsum2  20574  mdetdiag  20599  mdetunilem8  20619  mdetunilem9  20620  madurid  20644  mp2pm2mplem4  20808  fvmptnn04if  20848  fvmptnn04ifb  20850  elcls  21071  opnnei  21118  ist0-3  21343  ist1-2  21345  dfconn2  21416  cnconn  21419  pthaus  21635  xkohaus  21650  hausflim  21978  cldsubg  22107  bcth  23318  ioorinv  23536  tdeglem4  24011  fta1b  24120  plydivex  24243  plyexmo  24259  aalioulem3  24280  dvradcnv  24366  logtayllem  24596  logtayl  24597  cxpcl  24611  recxpcl  24612  logrec  24692  isosctrlem2  24740  efrlim  24887  muval2  25051  musum  25108  dchrelbas2  25153  dchrelbas4  25159  dchrfi  25171  dchrptlem3  25182  dchrsum2  25184  sumdchr2  25186  lgscllem  25220  2sqb  25348  dchrvmasumiflem2  25382  rpvmasum2  25392  padicabv  25510  padicabvf  25511  padicabvcxp  25512  tglowdim1i  25587  tgbtwnconn1  25661  colline  25735  colmid  25774  lmimid  25877  lmiisolem  25879  brbtwn2  25976  colinearalg  25981  axlowdimlem6  26018  axlowdimlem14  26026  axcontlem12  26046  incistruhgr  26165  umgr2edg1  26294  nb3grprlem1  26472  1egrvtxdg0  26609  vtxdginducedm1lem4  26640  wlkdlem4  26784  lfgriswlk  26787  pthdlem2  26866  wwlksnext  27003  clwwlknclwwlkdif  27092  clwlkclwwlklem2a4  27112  clwwisshclwwsn  27131  1wlkdlem4  27284  eupth2lem1  27362  eupth2lem3lem4  27375  frgr3vlem1  27419  frgr3vlem2  27420  3vfriswmgrlem  27423  4cycl2vnunb  27436  frgrncvvdeqlem8  27452  frgrregorufr  27471  frgrreg  27554  frgrregord013  27555  nvmul0or  27806  nmogtmnf  27926  hvmul0or  28183  hvmulcan  28230  hvmulcan2  28231  hiidge0  28256  bcsiALT  28337  shne0i  28608  nonbooli  28811  nmopgtmnf  29028  unopbd  29175  nmcfnlbi  29212  nmopcoi  29255  chirredi  29554  mdsymlem5  29567  sumdmdlem2  29579  disji2f  29689  imadifxp  29713  aciunf1  29764  2sqcoprm  29948  sitgaddlemb  30711  sgn3da  30904  plymulx  30926  bnj1109  31156  bnj1542  31226  bnj1253  31384  subfacp1lem6  31466  cvmsdisj  31551  sltval2  32107  sltres  32113  noseponlem  32115  nosepon  32116  nosepeq  32133  nosupbnd2lem1  32159  noetalem3  32163  btwnconn1lem13  32504  lineunray  32552  rankeq1o  32576  elicc3  32609  nn0prpw  32616  ordtoplem  32732  bj-ismooredr2  33363  bj-snmoore  33366  icorempt2  33502  matunitlindflem1  33710  poimirlem1  33715  poimirlem14  33728  poimirlem16  33730  poimirlem19  33733  poimirlem23  33737  poimirlem25  33739  poimirlem26  33740  itg2addnclem3  33768  itgaddnclem2  33774  fdc  33846  ismgmOLD  33954  cvrval2  35056  cvrnbtwn2  35057  cvrnbtwn3  35058  cvlsupr3  35126  cvrat4  35224  2at0mat0  35306  dalawlem13  35664  isltrn2N  35901  trlator0  35953  cdleme22b  36123  dochkrshp  37169  dochkrshp4  37172  lcfl6  37283  lclkrlem2x  37313  fphpd  37874  jm2.23  38057  sdrgacs  38265  isdomn3  38276  iunrelexp0  38488  ntrneineine1lem  38876  pm13.196a  39109  onfrALTlem5  39251  onfrALTlem3  39253  en3lpVD  39571  onfrALTlem5VD  39612  onfrALTlem3VD  39614  ax6e2ndeqVD  39636  ax6e2ndeqALT  39658  isosctrlem1ALT  39661  ndisj2  39709  limsupre2lem  40451  cncfiooicclem1  40601  iblcncfioo  40689  stoweidlem28  40740  sge0iunmpt  41130  raaan2  41673  afvfv0bi  41730  2ffzoeq  41840  iccpartiltu  41860  iccpartlt  41862  icceuelpartlem  41873  cshword2  41939  lighneallem4  42029  oddprmALTV  42100  evenprm2  42125  odd2prm2  42129  even3prm2  42130  upgrwlkupwlk  42223  copisnmnd  42311  pgrpgt2nabl  42649  islindeps  42744  lincext1  42745  lindslinindsimp2lem5  42753  snlindsntor  42762  ldepslinc  42800  m1modmmod  42818
  Copyright terms: Public domain W3C validator