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

Theorem neqned 3020
Description: If it is not the case that two classes are equal, then they are unequal. Converse of neneqd 3018. One-way deduction form of df-ne 3014. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 3039. (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 3014 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 235 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1528  wne 3013
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 208  df-ne 3014
This theorem is referenced by:  neqne  3021  necon3bi  3039  necon2ai  3042  necon3i  3045  nelne1  3110  nelne2  3112  mteqand  3119  ne0i  4297  nelpr2  4582  nelpr1  4583  otsndisj  5400  enpr2d  8585  sdomdif  8653  2pwne  8661  mapdom2  8676  canthp1lem2  10063  nnneneg  11660  flltnz  13169  wrdlen2i  14292  s3sndisj  14315  isprm2  16014  isprm5  16039  nnoddn2prmb  16138  hashfinmndnn  17916  sgrp2nmndlem5  18032  fincygsubgodd  19163  prmgrpsimpgd  19165  alexsub  22581  ioorf  24101  dvmptdiv  24498  dvtaylp  24885  cos02pilt1  25038  logccne0  25089  isosctrlem1  25323  isosctrlem2  25324  chordthmlem  25337  efrlim  25474  lgsfcl2  25806  lgscllem  25807  lgsval2lem  25810  2sqn0  25937  2sqmod  25939  dchrisumn0  26024  tgbtwnne  26203  tgbtwndiff  26219  tgbtwnconn1lem3  26287  legov3  26311  legso  26312  ncolne1  26338  tglineneq  26357  tglowdim2ln  26364  mirne  26380  miriso  26383  mirhl  26392  mirbtwnhl  26393  symquadlem  26402  krippenlem  26403  midexlem  26405  ragflat3  26419  ragperp  26430  footexALT  26431  footexlem2  26433  colperpexlem2  26444  colperpexlem3  26445  mideulem2  26447  oppne3  26456  outpasch  26468  hlpasch  26469  lmieu  26497  lmicom  26501  axlowdim1  26672  wlkp1lem5  27386  wlkp1lem6  27387  eulerpathpr  27946  nmcfnlbi  29756  strlem1  29954  unidifsnne  30223  fsuppcurry1  30387  fsuppcurry2  30388  divnumden2  30460  xrge0npcan  30608  tocyccntz  30713  ornglmullt  30807  orngrmullt  30808  qsidomlem1  30882  xrge0iifhom  31079  qqhf  31126  qqhre  31160  esumrnmpt2  31226  carsgclctunlem2  31476  ballotlemi1  31659  ballotlemii  31660  ballotlemfrcn0  31686  plymulx0  31716  signswn0  31729  signswch  31730  itgexpif  31776  repr0  31781  tgoldbachgtda  31831  pconnconn  32375  noseponlem  33068  nosupbnd1lem3  33107  nosupbnd1lem4  33108  nosupbnd1lem5  33109  nosupbnd2lem1  33112  unbdqndv2lem2  33746  knoppndvlem13  33760  sucneqond  34528  finxpreclem2  34553  finxp1o  34555  maxidln0  35204  hdmapip0  38931  remul01  39115  3cubeslem4  39164  3cubes  39165  pellexlem6  39309  scotteld  40459  mnuprdlem2  40486  inaex  40510  n0p  41182  disjrnmpt2  41325  rnmptn0  41360  dstregt0  41423  upbdrech2  41451  xrlexaddrp  41496  infleinflem2  41515  xrralrecnnge  41538  supminfxr2  41621  absimnre  41629  xrpnf  41638  ressioosup  41707  ressiooinf  41709  fmul01lt1lem1  41741  limcperiod  41785  climxrrelem  41906  sinaover2ne0  42025  fperdvper  42079  dvdivbd  42084  itgioocnicc  42138  stirlinglem5  42240  dirker2re  42254  dirkerdenne0  42255  dirkerper  42258  dirkertrigeqlem3  42262  dirkertrigeq  42263  dirkercncflem1  42265  dirkercncflem2  42266  dirkercncflem4  42268  fourierdlem24  42293  fourierdlem25  42294  fourierdlem40  42309  fourierdlem41  42310  fourierdlem42  42311  fourierdlem44  42313  fourierdlem48  42316  fourierdlem49  42317  fourierdlem57  42325  fourierdlem58  42326  fourierdlem59  42327  fourierdlem66  42334  fourierdlem68  42336  fourierdlem74  42342  fourierdlem75  42343  fourierdlem78  42346  fourierdlem80  42348  fourierdlem81  42349  fourierdlem109  42377  elaa2lem  42395  etransclem9  42405  etransclem35  42431  etransclem38  42434  sge0tsms  42539  sge0cl  42540  sge0fodjrnlem  42575  meadjun  42621  meadjiunlem  42624  hoicvr  42707  hoidmvlelem2  42755  hoiqssbllem3  42783  sigardiv  42995  sigarcol  42998  sharhght  42999  prmdvdsfmtnof1lem2  43624  difmodm1lt  44510
  Copyright terms: Public domain W3C validator