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

Step	Hyp	Ref	Expression
1		moim 2507	. 2 ⊢ (∀𝑥(𝜑 → 𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
2		moimi.1	. 2 ⊢ (𝜑 → 𝜓)
3	1, 2	mpg 1715	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

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