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

Theorem moimi 2549
 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 2548 . 2 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2 moimi.1 . 2 (𝜑𝜓)
31, 2mpg 1764 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃*wmo 2499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-eu 2502  df-mo 2503 This theorem is referenced by:  moa1  2550  moan  2553  moor  2555  mooran1  2556  mooran2  2557  moaneu  2562  2moex  2572  2euex  2573  2exeu  2578  sndisj  4676  disjxsn  4678  fununmo  5971  funcnvsn  5974  nfunsn  6263  caovmo  6913  iunmapdisj  8884  brdom3  9388  brdom5  9389  brdom4  9390  nqerf  9790  shftfn  13857  2ndcdisj2  21308  plyexmo  24113  ajfuni  27843  funadj  28873  cnlnadjeui  29064
 Copyright terms: Public domain W3C validator