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

Theorem neqned 2903
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2901. One-way deduction form of df-ne 2897. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2922. (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 2897 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 224 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1596  wne 2896
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 2897
This theorem is referenced by:  neqne  2904  necon3bi  2922  necon2ai  2925  necon3i  2928  ne0i  4029  otsndisj  5083  sdomdif  8224  2pwne  8232  mapdom2  8247  canthp1lem2  9588  xrge0neqmnf  12390  flltnz  12727  wrdlen2i  13808  s3sndisj  13828  isprm2  15518  isprm5  15542  nnoddn2prmb  15641  sgrp2nmndlem5  17538  maducoeval2  20569  alexsub  21971  ioorf  23462  dvmptdiv  23857  dvtaylp  24244  logccne0  24445  isosctrlem1  24668  isosctrlem2  24669  chordthmlem  24679  efrlim  24816  lgsfcl2  25148  lgscllem  25149  lgsval2lem  25152  dchrisumn0  25330  tgbtwnne  25505  tgbtwndiff  25521  tgbtwnconn1lem3  25589  legov3  25613  legso  25614  ncolne1  25640  tglineneq  25659  tglowdim2ln  25666  mirne  25682  miriso  25685  mirhl  25694  mirbtwnhl  25695  symquadlem  25704  krippenlem  25705  midexlem  25707  ragflat3  25721  ragperp  25732  footex  25733  colperpexlem2  25743  colperpexlem3  25744  mideulem2  25746  oppne3  25755  outpasch  25767  hlpasch  25768  lmieu  25796  lmicom  25800  axlowdim1  25959  nbgrssovtxOLD  26380  wlkp1lem5  26705  wlkp1lem6  26706  eulerpathpr  27313  nmcfnlbi  29141  strlem1  29339  divnumden2  29794  2sqn0  29876  2sqmod  29878  xrge0npcan  29924  ornglmullt  30037  orngrmullt  30038  xrge0iifhom  30213  qqhf  30260  qqhre  30294  esumrnmpt2  30360  carsgclctunlem2  30611  ballotlemi1  30794  ballotlemii  30795  ballotlemfrcn0  30821  plymulx0  30854  signswn0  30867  signswch  30868  signstfvneq0  30879  itgexpif  30914  repr0  30919  tgoldbachgtda  30969  pconnconn  31441  noseponlem  32044  nosupbnd1lem3  32083  nosupbnd1lem4  32084  nosupbnd1lem5  32085  nosupbnd2lem1  32088  unbdqndv2lem2  32728  knoppndvlem13  32742  sucneqond  33445  finxpreclem2  33459  finxp1o  33461  maxidln0  34076  hdmapip0  37626  pellexlem6  37817  n0p  39625  nelpr2  39677  nelpr1  39678  disjrnmpt2  39791  rnmptn0  39829  dstregt0  39909  upbdrech2  39938  xrlexaddrp  39983  infleinflem2  40002  xrralrecnnge  40028  supminfxr2  40114  absimnre  40122  xrpnf  40131  ressioosup  40202  ressiooinf  40204  fmul01lt1lem1  40236  limcperiod  40280  climxrrelem  40401  sinaover2ne0  40499  fperdvper  40553  dvdivbd  40558  itgioocnicc  40613  stirlinglem5  40715  dirker2re  40729  dirkerdenne0  40730  dirkerper  40733  dirkertrigeqlem3  40737  dirkertrigeq  40738  dirkercncflem1  40740  dirkercncflem2  40741  dirkercncflem4  40743  fourierdlem24  40768  fourierdlem25  40769  fourierdlem40  40784  fourierdlem41  40785  fourierdlem42  40786  fourierdlem44  40788  fourierdlem48  40791  fourierdlem49  40792  fourierdlem57  40800  fourierdlem58  40801  fourierdlem59  40802  fourierdlem66  40809  fourierdlem68  40811  fourierdlem74  40817  fourierdlem75  40818  fourierdlem78  40821  fourierdlem80  40823  fourierdlem81  40824  fourierdlem109  40852  elaa2lem  40870  etransclem9  40880  etransclem35  40906  etransclem38  40909  sge0tsms  41017  sge0cl  41018  sge0fodjrnlem  41053  meadjun  41099  meadjiunlem  41102  hoicvr  41185  hoidmvlelem2  41233  hoiqssbllem3  41261  sigardiv  41473  sigarcol  41476  sharhght  41477  prmdvdsfmtnof1lem2  41924  difmodm1lt  42744
  Copyright terms: Public domain W3C validator