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

Theorem moimi 2669
Description: "At most one" reverses implication. (Contributed by NM, 15-Feb-2006.)
Hypothesis
Ref Expression
moimi.1 (𝜑𝜓)
Assertion
Ref Expression
moimi (∃*𝑥𝜓 → ∃*𝑥𝜑)

Proof of Theorem moimi
StepHypRef Expression
1 moim 2668 . 2 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2 moimi.1 . 2 (𝜑𝜓)
31, 2mpg 1872 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ∃*wmo 2619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-12 2203
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ex 1853  df-nf 1858  df-eu 2622  df-mo 2623
This theorem is referenced by:  moa1  2670  moan  2673  moor  2675  mooran1  2676  mooran2  2677  moaneu  2682  2moex  2692  2euex  2693  2exeu  2698  sndisj  4778  disjxsn  4780  fununmo  6074  funcnvsn  6077  nfunsn  6365  caovmo  7018  iunmapdisj  9046  brdom3  9552  brdom5  9553  brdom4  9554  nqerf  9954  shftfn  14017  2ndcdisj2  21477  plyexmo  24284  ajfuni  28051  funadj  29081  cnlnadjeui  29272
  Copyright terms: Public domain W3C validator