Definition df-ne 2795

Description: Define inequality. (Contributed by NM, 26-May-1993.)

Assertion

Ref	Expression
df-ne	|- ( A =/= B <-> -. A = B )

Detailed syntax breakdown of Definition df-ne

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	wne 2794	. 2 wff A =/= B
4	1, 2	wceq 1483	. . 3 wff A = B
5	4	wn 3	. 2 wff -. A = B
6	3, 5	wb 196	1 wff ( A =/= B <-> -. A = B )

This definition is referenced by:  neii  2796  neir  2797  nne  2798  neneqd  2799  neqned  2801  eqneqall  2805  necon2bd  2810  necon1bd  2812  necon3d  2815  necon2d  2817  necon1bi  2822  necon1i  2827  necon3abid  2830  necon1bbid  2833  necon3bid  2838  necon3abii  2840  necon3bii  2846  neor  2885  neanior  2886  neorian  2888  nfne  2894  nfned  2895  nabbi  2896  dfpss2  3692  n0f  3927  ifnefalse  4098  snnzb  4254  raldifsni  4324  eqsn  4361  eqsnOLD  4362  n0snor2el  4364  opthpr  4384  unissint  4501  iununi  4610  disji2  4636  opthneg  4950  opab0  5007  xpcan  5570  xpcan2  5571  xpima  5576  unixpid  5670  unizlim  5844  2f1fvneq  6517  dff14a  6527  orduniorsuc  7030  dflim3  7047  tfindsg  7060  nn0suc  7090  findsg  7093  suppvalbr  7299  wfrlem16  7430  tz7.49  7540  oevn0  7595  php  8144  1sdom  8163  fimaxg  8207  fiint  8237  wemapsolem  8455  card2on  8459  brwdomn0  8474  domwdom  8479  rankxplim2  8743  rankxplim3  8744  carden2a  8792  dfackm  8988  fin23lem14  9155  fin1a2lem12  9233  axcc2lem  9258  ac6num  9301  zorn2lem4  9321  zorn2lem7  9324  brdom3  9350  iundom2g  9362  r1tskina  9604  1re  10039  ltlen  10138  uzm1  11718  xrnemnf  11951  xrnepnf  11952  ioo0  12200  ico0  12221  ioc0  12222  icc0  12223  elfznelfzo  12573  elfznelfzob  12574  injresinjlem  12588  fleqceilz  12653  fsuppmapnn0fiubex  12792  sq01  12986  hash1snb  13207  hashgt12el  13210  hashgt12el2  13211  hashfun  13224  hash2prde  13252  hashge2el2dif  13262  fundmge2nop0  13274  swrdccatin1  13483  repswcshw  13558  cshw1  13568  xptrrel  13719  incexc2  14570  sqrt2irr  14979  divalglem8  15123  ndvdssub  15133  algcvgblem  15290  lcmcllem  15309  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  ncoprmgcdne1b  15363  isprm3  15396  isprm4  15397  ramcl2lem  15713  cshwshashlem1  15802  cshwshash  15811  sgrp2nmndlem3  17412  sgrp2rid2  17413  sgrp2nmndlem5  17416  symg2bas  17818  symgextf  17837  symgextfv  17838  odlem1  17954  gexlem1  17994  dprdfeq0  18421  isnirred  18700  isirred2  18701  drngmul0or  18768  drngmuleq0  18770  lvecvs0or  19108  lvecvscan  19111  isnzr2  19263  isdomn2  19299  cply1mul  19664  gsummoncoe1  19674  domnchr  19880  psgndiflemB  19946  dmatmul  20303  mulmarep1gsum1  20379  mulmarep1gsum2  20380  mdetdiag  20405  mdetunilem8  20425  mdetunilem9  20426  madurid  20450  mp2pm2mplem4  20614  fvmptnn04if  20654  fvmptnn04ifb  20656  elcls  20877  opnnei  20924  ist0-3  21149  ist1-2  21151  dfconn2  21222  cnconn  21225  pthaus  21441  xkohaus  21456  hausflim  21785  cldsubg  21914  bcth  23126  ioorinv  23344  tdeglem4  23820  fta1b  23929  plydivex  24052  plyexmo  24068  aalioulem3  24089  dvradcnv  24175  logtayllem  24405  logtayl  24406  cxpcl  24420  recxpcl  24421  logrec  24501  isosctrlem2  24549  efrlim  24696  muval2  24860  musum  24917  dchrelbas2  24962  dchrelbas4  24968  dchrfi  24980  dchrptlem3  24991  dchrsum2  24993  sumdchr2  24995  lgscllem  25029  2sqb  25157  dchrvmasumiflem2  25191  rpvmasum2  25201  padicabv  25319  padicabvf  25320  padicabvcxp  25321  tglowdim1i  25396  tgbtwnconn1  25470  colline  25544  colmid  25583  lmimid  25686  lmiisolem  25688  brbtwn2  25785  colinearalg  25790  axlowdimlem6  25827  axlowdimlem14  25835  axcontlem12  25855  incistruhgr  25974  umgr2edg1  26103  nb3grprlem1  26282  1egrvtxdg0  26407  vtxdginducedm1lem4  26438  wlkdlem4  26582  lfgriswlk  26585  pthdlem2  26664  wwlksnext  26788  clwlkclwwlklem2a4  26898  clwwisshclwwsn  26929  1wlkdlem4  27000  eupth2lem1  27078  eupth2lem3lem4  27091  frgr3vlem1  27137  frgr3vlem2  27138  3vfriswmgrlem  27141  4cycl2vnunb  27154  frgrncvvdeqlem8  27170  frgrregorufr  27189  frgrreg  27252  frgrregord013  27253  nvmul0or  27505  nmogtmnf  27625  hvmul0or  27882  hvmulcan  27929  hvmulcan2  27930  hiidge0  27955  bcsiALT  28036  shne0i  28307  nonbooli  28510  nmopgtmnf  28727  unopbd  28874  nmcfnlbi  28911  nmopcoi  28954  chirredi  29253  mdsymlem5  29266  sumdmdlem2  29278  disji2f  29390  imadifxp  29414  aciunf1  29463  2sqcoprm  29647  sitgaddlemb  30410  sgn3da  30603  plymulx  30625  bnj1109  30857  bnj1542  30927  bnj1253  31085  subfacp1lem6  31167  cvmsdisj  31252  sltval2  31809  sltres  31815  noseponlem  31817  nosepon  31818  nosepeq  31835  nosupbnd2lem1  31861  noetalem3  31865  btwnconn1lem13  32206  lineunray  32254  rankeq1o  32278  elicc3  32311  nn0prpw  32318  ordtoplem  32434  bj-ismooredr2  33065  bj-snmoore  33068  icorempt2  33199  matunitlindflem1  33405  poimirlem1  33410  poimirlem14  33423  poimirlem16  33425  poimirlem19  33428  poimirlem23  33432  poimirlem25  33434  poimirlem26  33435  itg2addnclem3  33463  itgaddnclem2  33469  fdc  33541  ismgmOLD  33649  cvrval2  34561  cvrnbtwn2  34562  cvrnbtwn3  34563  cvlsupr3  34631  cvrat4  34729  2at0mat0  34811  dalawlem13  35169  isltrn2N  35406  trlator0  35458  cdleme22b  35629  dochkrshp  36675  dochkrshp4  36678  lcfl6  36789  lclkrlem2x  36819  fphpd  37380  jm2.23  37563  sdrgacs  37771  isdomn3  37782  iunrelexp0  37994  ntrneineine1lem  38382  pm13.196a  38615  onfrALTlem5  38757  onfrALTlem3  38759  en3lpVD  39080  onfrALTlem5VD  39121  onfrALTlem3VD  39123  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  isosctrlem1ALT  39170  ndisj2  39218  limsupre2lem  39956  cncfiooicclem1  40106  iblcncfioo  40194  stoweidlem28  40245  sge0iunmpt  40635  raaan2  41175  afvfv0bi  41232  2ffzoeq  41338  iccpartiltu  41358  iccpartlt  41360  icceuelpartlem  41371  cshword2  41437  lighneallem4  41527  oddprmALTV  41598  evenprm2  41623  odd2prm2  41627  even3prm2  41628  upgrwlkupwlk  41721  copisnmnd  41809  pgrpgt2nabl  42147  islindeps  42242  lincext1  42243  lindslinindsimp2lem5  42251  snlindsntor  42260  ldepslinc  42298  m1modmmod  42316