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

Theorem neqned 2789
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2787. One-way deduction form of df-ne 2782. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2808. (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 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 223 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1475  wne 2780
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 196  df-ne 2782
This theorem is referenced by:  neqne  2790  necon3bi  2808  necon2ai  2811  necon3i  2814  ne0i  3880  otsndisj  4904  sdomdif  7993  2pwne  8001  mapdom2  8016  canthp1lem2  9354  xrge0neqmnf  12147  flltnz  12474  wrdlen2i  13534  s3sndisj  13554  isprm2  15233  isprm5  15257  nnoddn2prmb  15356  sgrp2nmndlem5  17239  maducoeval2  20265  alexsub  21659  ioorf  23147  dvtaylp  23928  logccne0  24129  isosctrlem1  24348  isosctrlem2  24349  chordthmlem  24359  efrlim  24496  lgsfcl2  24828  lgscllem  24829  lgsval2lem  24832  dchrisumn0  25010  tgbtwnne  25185  tgbtwndiff  25201  tgbtwnconn1lem3  25269  legov3  25293  legso  25294  ncolne1  25320  tglineneq  25339  tglowdim2ln  25346  mirne  25362  miriso  25365  mirhl  25374  mirbtwnhl  25375  symquadlem  25384  krippenlem  25385  midexlem  25387  ragflat3  25401  ragperp  25412  footex  25413  colperpexlem2  25423  colperpexlem3  25424  mideulem2  25426  oppne3  25435  outpasch  25447  hlpasch  25448  lmieu  25476  lmicom  25480  axlowdim1  25639  eupath  26508  nmcfnlbi  28295  strlem1  28493  divnumden2  28951  2sqn0  28977  2sqmod  28979  xrge0npcan  29025  ornglmullt  29138  orngrmullt  29139  xrge0iifhom  29311  qqhf  29358  qqhre  29392  esumrnmpt2  29457  carsgclctunlem2  29708  ballotlemi1  29891  ballotlemii  29892  ballotlemfrcn0  29918  plymulx0  29950  signswn0  29963  signswch  29964  signstfvneq0  29975  pconcon  30467  noseponlem  31065  nodenselem3  31082  unbdqndv2lem2  31671  knoppndvlem13  31685  sucneqond  32389  finxpreclem2  32403  finxp1o  32405  maxidln0  33014  hdmapip0  36225  pellexlem6  36416  n0p  38234  nelpr2  38288  nelpr1  38289  disjrnmpt2  38370  rnmptn0  38408  dstregt0  38434  upbdrech2  38463  xrlexaddrp  38509  infleinflem2  38528  xrralrecnnge  38554  ressioosup  38629  ressiooinf  38631  fmul01lt1lem1  38651  limcperiod  38695  sinaover2ne0  38751  dvmptdiv  38807  fperdvper  38808  dvdivbd  38813  itgioocnicc  38869  stirlinglem5  38971  dirker2re  38985  dirkerdenne0  38986  dirkerper  38989  dirkertrigeqlem3  38993  dirkertrigeq  38994  dirkercncflem1  38996  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem24  39024  fourierdlem25  39025  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem44  39044  fourierdlem48  39047  fourierdlem49  39048  fourierdlem57  39056  fourierdlem58  39057  fourierdlem59  39058  fourierdlem66  39065  fourierdlem68  39067  fourierdlem74  39073  fourierdlem75  39074  fourierdlem78  39077  fourierdlem80  39079  fourierdlem81  39080  fourierdlem109  39108  elaa2lem  39126  etransclem9  39136  etransclem35  39162  etransclem38  39165  sge0tsms  39273  sge0cl  39274  sge0fodjrnlem  39309  meadjun  39355  meadjiunlem  39358  hoicvr  39438  hoidmvlelem2  39486  hoiqssbllem3  39514  sigardiv  39699  sigarcol  39702  sharhght  39703  prmdvdsfmtnof1lem2  40035  nbgrssovtx  40586  1wlkp1lem5  40886  1wlkp1lem6  40887  eulerpathpr  41408  difmodm1lt  42111
  Copyright terms: Public domain W3C validator