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

Theorem moimi 2690
Description: The at-most-one quantifier 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 2689 . 2 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2 moimi.1 . 2 (𝜑𝜓)
31, 2mpg 1879 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ∃*wmo 2633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001
This theorem depends on definitions:  df-bi 198  df-ex 1860  df-mo 2635
This theorem is referenced by:  moa1  2692  moan  2695  moor  2697  mooran1  2698  mooran2  2699  moaneu  2704  2moex  2714  2euex  2715  2exeu  2720  sndisj  4843  disjxsn  4845  fununmo  6150  funcnvsn  6153  nfunsn  6448  caovmo  7104  iunmapdisj  9132  brdom3  9638  brdom5  9639  brdom4  9640  nqerf  10040  shftfn  14039  2ndcdisj2  21478  plyexmo  24288  ajfuni  28049  funadj  29079  cnlnadjeui  29270  funressnvmo  41665
  Copyright terms: Public domain W3C validator