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

Theorem moimi 2508
 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 2507 . 2 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2 moimi.1 . 2 (𝜑𝜓)
31, 2mpg 1715 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃*wmo 2459 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463 This theorem is referenced by:  moa1  2509  moan  2512  moor  2514  mooran1  2515  mooran2  2516  moaneu  2521  2moex  2531  2euex  2532  2exeu  2537  sndisj  4574  disjxsn  4576  fununmo  5847  funcnvsn  5850  nfunsn  6135  caovmo  6769  iunmapdisj  8729  brdom3  9231  brdom5  9232  brdom4  9233  nqerf  9631  shftfn  13661  2ndcdisj2  21070  plyexmo  23872  ajfuni  27099  funadj  28129  cnlnadjeui  28320
 Copyright terms: Public domain W3C validator