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

Theorem neqned 3021
Description: If it is not the case that two classes are equal, then they are unequal. Converse of neneqd 3019. One-way deduction form of df-ne 3015. (Contributed by David Moews, 28-Feb-2017.) Allow a shortening of necon3bi 3040. (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 3015 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylibr 236 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1530  wne 3014
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 209  df-ne 3015
This theorem is referenced by:  neqne  3022  necon3bi  3040  necon2ai  3043  necon3i  3046  nelne1  3111  nelne2  3113  mteqand  3120  ne0i  4298  nelpr2  4584  nelpr1  4585  otsndisj  5400  enpr2d  8589  sdomdif  8657  2pwne  8665  mapdom2  8680  canthp1lem2  10067  nnneneg  11664  flltnz  13173  wrdlen2i  14296  s3sndisj  14319  isprm2  16018  isprm5  16043  nnoddn2prmb  16142  hashfinmndnn  17920  sgrp2nmndlem5  18086  fincygsubgodd  19226  prmgrpsimpgd  19228  alexsub  22645  ioorf  24166  dvmptdiv  24563  dvtaylp  24950  cos02pilt1  25103  logccne0  25154  isosctrlem1  25388  isosctrlem2  25389  chordthmlem  25402  efrlim  25539  lgsfcl2  25871  lgscllem  25872  lgsval2lem  25875  2sqn0  26002  2sqmod  26004  dchrisumn0  26089  tgbtwnne  26268  tgbtwndiff  26284  tgbtwnconn1lem3  26352  legov3  26376  legso  26377  ncolne1  26403  tglineneq  26422  tglowdim2ln  26429  mirne  26445  miriso  26448  mirhl  26457  mirbtwnhl  26458  symquadlem  26467  krippenlem  26468  midexlem  26470  ragflat3  26484  ragperp  26495  footexALT  26496  footexlem2  26498  colperpexlem2  26509  colperpexlem3  26510  mideulem2  26512  oppne3  26521  outpasch  26533  hlpasch  26534  lmieu  26562  lmicom  26566  axlowdim1  26737  wlkp1lem5  27451  wlkp1lem6  27452  eulerpathpr  28011  nmcfnlbi  29821  strlem1  30019  unidifsnne  30288  fsuppcurry1  30453  fsuppcurry2  30454  divnumden2  30526  xrge0npcan  30674  tocyccntz  30779  ornglmullt  30873  orngrmullt  30874  qsidomlem1  30957  xrge0iifhom  31168  qqhf  31215  qqhre  31249  esumrnmpt2  31315  carsgclctunlem2  31565  ballotlemi1  31748  ballotlemii  31749  ballotlemfrcn0  31775  plymulx0  31805  signswn0  31818  signswch  31819  itgexpif  31865  repr0  31870  tgoldbachgtda  31920  pconnconn  32466  noseponlem  33159  nosupbnd1lem3  33198  nosupbnd1lem4  33199  nosupbnd1lem5  33200  nosupbnd2lem1  33203  unbdqndv2lem2  33837  knoppndvlem13  33851  sucneqond  34628  finxpreclem2  34653  finxp1o  34655  maxidln0  35305  hdmapip0  39033  remul01  39217  3cubeslem4  39266  3cubes  39267  pellexlem6  39411  scotteld  40562  mnuprdlem2  40589  inaex  40613  n0p  41285  disjrnmpt2  41428  rnmptn0  41463  dstregt0  41526  upbdrech2  41554  xrlexaddrp  41599  infleinflem2  41618  xrralrecnnge  41641  supminfxr2  41724  absimnre  41732  xrpnf  41741  ressioosup  41810  ressiooinf  41812  fmul01lt1lem1  41844  limcperiod  41888  climxrrelem  42009  sinaover2ne0  42128  fperdvper  42182  dvdivbd  42187  itgioocnicc  42241  stirlinglem5  42343  dirker2re  42357  dirkerdenne0  42358  dirkerper  42361  dirkertrigeqlem3  42365  dirkertrigeq  42366  dirkercncflem1  42368  dirkercncflem2  42369  dirkercncflem4  42371  fourierdlem24  42396  fourierdlem25  42397  fourierdlem40  42412  fourierdlem41  42413  fourierdlem42  42414  fourierdlem44  42416  fourierdlem48  42419  fourierdlem49  42420  fourierdlem57  42428  fourierdlem58  42429  fourierdlem59  42430  fourierdlem66  42437  fourierdlem68  42439  fourierdlem74  42445  fourierdlem75  42446  fourierdlem78  42449  fourierdlem80  42451  fourierdlem81  42452  fourierdlem109  42480  elaa2lem  42498  etransclem9  42508  etransclem35  42534  etransclem38  42537  sge0tsms  42642  sge0cl  42643  sge0fodjrnlem  42678  meadjun  42724  meadjiunlem  42727  hoicvr  42810  hoidmvlelem2  42858  hoiqssbllem3  42886  sigardiv  43098  sigarcol  43101  sharhght  43102  prmdvdsfmtnof1lem2  43727  difmodm1lt  44562
  Copyright terms: Public domain W3C validator