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

Theorem neqned 2797
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2795. One-way deduction form of df-ne 2791. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2816. (Revised by Wolf Lammen, 22-Nov-2019.)
Hypothesis
Ref Expression
neqned.1 (𝜑 → ¬ 𝐴 = 𝐵)
Assertion
Ref Expression
neqned (𝜑𝐴𝐵)

Proof of Theorem neqned
StepHypRef Expression
1 neqned.1 . 2 (𝜑 → ¬ 𝐴 = 𝐵)
2 df-ne 2791 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 224 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1480  wne 2790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-ne 2791
This theorem is referenced by:  neqne  2798  necon3bi  2816  necon2ai  2819  necon3i  2822  ne0i  3899  otsndisj  4941  sdomdif  8055  2pwne  8063  mapdom2  8078  canthp1lem2  9422  xrge0neqmnf  12221  flltnz  12555  wrdlen2i  13623  s3sndisj  13643  isprm2  15322  isprm5  15346  nnoddn2prmb  15445  sgrp2nmndlem5  17340  maducoeval2  20368  alexsub  21762  ioorf  23254  dvtaylp  24035  logccne0  24236  isosctrlem1  24455  isosctrlem2  24456  chordthmlem  24466  efrlim  24603  lgsfcl2  24935  lgscllem  24936  lgsval2lem  24939  dchrisumn0  25117  tgbtwnne  25292  tgbtwndiff  25308  tgbtwnconn1lem3  25376  legov3  25400  legso  25401  ncolne1  25427  tglineneq  25446  tglowdim2ln  25453  mirne  25469  miriso  25472  mirhl  25481  mirbtwnhl  25482  symquadlem  25491  krippenlem  25492  midexlem  25494  ragflat3  25508  ragperp  25519  footex  25520  colperpexlem2  25530  colperpexlem3  25531  mideulem2  25533  oppne3  25542  outpasch  25554  hlpasch  25555  lmieu  25583  lmicom  25587  axlowdim1  25746  nbgrssovtx  26154  wlkp1lem5  26450  wlkp1lem6  26451  eulerpathpr  26973  nmcfnlbi  28772  strlem1  28970  divnumden2  29417  2sqn0  29443  2sqmod  29445  xrge0npcan  29491  ornglmullt  29604  orngrmullt  29605  xrge0iifhom  29777  qqhf  29824  qqhre  29858  esumrnmpt2  29923  carsgclctunlem2  30174  ballotlemi1  30357  ballotlemii  30358  ballotlemfrcn0  30384  plymulx0  30416  signswn0  30429  signswch  30430  signstfvneq0  30441  itgexpif  30463  pconnconn  30942  noseponlem  31543  nodenselem3  31567  unbdqndv2lem2  32164  knoppndvlem13  32178  sucneqond  32866  finxpreclem2  32880  finxp1o  32882  maxidln0  33497  hdmapip0  36708  pellexlem6  36899  n0p  38713  nelpr2  38765  nelpr1  38766  disjrnmpt2  38867  rnmptn0  38905  dstregt0  38975  upbdrech2  39004  xrlexaddrp  39050  infleinflem2  39069  xrralrecnnge  39095  ressioosup  39211  ressiooinf  39213  fmul01lt1lem1  39238  limcperiod  39282  sinaover2ne0  39400  dvmptdiv  39455  fperdvper  39456  dvdivbd  39461  itgioocnicc  39516  stirlinglem5  39618  dirker2re  39632  dirkerdenne0  39633  dirkerper  39636  dirkertrigeqlem3  39640  dirkertrigeq  39641  dirkercncflem1  39643  dirkercncflem2  39644  dirkercncflem4  39646  fourierdlem24  39671  fourierdlem25  39672  fourierdlem40  39687  fourierdlem41  39688  fourierdlem42  39689  fourierdlem44  39691  fourierdlem48  39694  fourierdlem49  39695  fourierdlem57  39703  fourierdlem58  39704  fourierdlem59  39705  fourierdlem66  39712  fourierdlem68  39714  fourierdlem74  39720  fourierdlem75  39721  fourierdlem78  39724  fourierdlem80  39726  fourierdlem81  39727  fourierdlem109  39755  elaa2lem  39773  etransclem9  39783  etransclem35  39809  etransclem38  39812  sge0tsms  39920  sge0cl  39921  sge0fodjrnlem  39956  meadjun  40002  meadjiunlem  40005  hoicvr  40085  hoidmvlelem2  40133  hoiqssbllem3  40161  sigardiv  40370  sigarcol  40373  sharhght  40374  prmdvdsfmtnof1lem2  40812  difmodm1lt  41621
  Copyright terms: Public domain W3C validator