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

Theorem moimi 2507
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 2506 . 2 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2 moimi.1 . 2 (𝜑𝜓)
31, 2mpg 1714 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  ∃*wmo 2458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-12 2033
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-eu 2461  df-mo 2462
This theorem is referenced by:  moa1  2508  moan  2511  moor  2513  mooran1  2514  mooran2  2515  moaneu  2520  2moex  2530  2euex  2531  2exeu  2536  sndisj  4568  disjxsn  4570  fununmo  5832  funcnvsn  5835  nfunsn  6119  caovmo  6746  iunmapdisj  8706  brdom3  9208  brdom5  9209  brdom4  9210  nqerf  9608  shftfn  13609  2ndcdisj2  21017  plyexmo  23816  ajfuni  26892  funadj  27922  cnlnadjeui  28113
  Copyright terms: Public domain W3C validator