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

Theorem neqned 2950
Description: If it is not the case that two classes are equal, they are unequal. Converse of neneqd 2948. One-way deduction form of df-ne 2944. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 2969. (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 2944 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 224 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1631  wne 2943
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 2944
This theorem is referenced by:  neqne  2951  necon3bi  2969  necon2ai  2972  necon3i  2975  ne0i  4069  otsndisj  5112  sdomdif  8262  2pwne  8270  mapdom2  8285  canthp1lem2  9675  xrge0neqmnfOLD  12476  flltnz  12813  wrdlen2i  13889  s3sndisj  13909  isprm2  15595  isprm5  15619  nnoddn2prmb  15718  sgrp2nmndlem5  17617  maducoeval2  20657  alexsub  22062  ioorf  23554  dvmptdiv  23950  dvtaylp  24337  logccne0  24539  isosctrlem1  24762  isosctrlem2  24763  chordthmlem  24773  efrlim  24910  lgsfcl2  25242  lgscllem  25243  lgsval2lem  25246  dchrisumn0  25424  tgbtwnne  25599  tgbtwndiff  25615  tgbtwnconn1lem3  25683  legov3  25707  legso  25708  ncolne1  25734  tglineneq  25753  tglowdim2ln  25760  mirne  25776  miriso  25779  mirhl  25788  mirbtwnhl  25789  symquadlem  25798  krippenlem  25799  midexlem  25801  ragflat3  25815  ragperp  25826  footex  25827  colperpexlem2  25837  colperpexlem3  25838  mideulem2  25840  oppne3  25849  outpasch  25861  hlpasch  25862  lmieu  25890  lmicom  25894  axlowdim1  26053  nbgrssovtxOLD  26476  wlkp1lem5  26802  wlkp1lem6  26803  eulerpathpr  27413  nmcfnlbi  29244  strlem1  29442  divnumden2  29897  2sqn0  29979  2sqmod  29981  xrge0npcan  30027  ornglmullt  30140  orngrmullt  30141  xrge0iifhom  30316  qqhf  30363  qqhre  30397  esumrnmpt2  30463  carsgclctunlem2  30714  ballotlemi1  30897  ballotlemii  30898  ballotlemfrcn0  30924  plymulx0  30957  signswn0  30970  signswch  30971  signstfvneq0  30982  itgexpif  31017  repr0  31022  tgoldbachgtda  31072  pconnconn  31544  noseponlem  32147  nosupbnd1lem3  32186  nosupbnd1lem4  32187  nosupbnd1lem5  32188  nosupbnd2lem1  32191  unbdqndv2lem2  32831  knoppndvlem13  32845  sucneqond  33543  finxpreclem2  33557  finxp1o  33559  maxidln0  34169  hdmapip0  37718  pellexlem6  37917  n0p  39723  nelpr2  39775  nelpr1  39776  disjrnmpt2  39888  rnmptn0  39924  dstregt0  40004  upbdrech2  40032  xrlexaddrp  40077  infleinflem2  40096  xrralrecnnge  40122  supminfxr2  40208  absimnre  40216  xrpnf  40225  ressioosup  40293  ressiooinf  40295  fmul01lt1lem1  40327  limcperiod  40371  climxrrelem  40492  sinaover2ne0  40590  fperdvper  40644  dvdivbd  40649  itgioocnicc  40703  stirlinglem5  40805  dirker2re  40819  dirkerdenne0  40820  dirkerper  40823  dirkertrigeqlem3  40827  dirkertrigeq  40828  dirkercncflem1  40830  dirkercncflem2  40831  dirkercncflem4  40833  fourierdlem24  40858  fourierdlem25  40859  fourierdlem40  40874  fourierdlem41  40875  fourierdlem42  40876  fourierdlem44  40878  fourierdlem48  40881  fourierdlem49  40882  fourierdlem57  40890  fourierdlem58  40891  fourierdlem59  40892  fourierdlem66  40899  fourierdlem68  40901  fourierdlem74  40907  fourierdlem75  40908  fourierdlem78  40911  fourierdlem80  40913  fourierdlem81  40914  fourierdlem109  40942  elaa2lem  40960  etransclem9  40970  etransclem35  40996  etransclem38  40999  sge0tsms  41107  sge0cl  41108  sge0fodjrnlem  41143  meadjun  41189  meadjiunlem  41192  hoicvr  41275  hoidmvlelem2  41323  hoiqssbllem3  41351  sigardiv  41563  sigarcol  41566  sharhght  41567  prmdvdsfmtnof1lem2  42018  difmodm1lt  42838
  Copyright terms: Public domain W3C validator