Theorem moimi 2573

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

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

This proof depends on syntax axioms:   → wi 4  ∃*wmo 2565

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-mo 2567

This theorem is used by:  moa1  2579  moan  2580  moor  2582  mooran1  2583  mooran2  2584  moaneu  2651  2moexv  2655  2euexv  2659  2exeuv  2660  2moex  2668  2euex  2669  2exeu  2674  sndisj  5098  disjxsn  5100  axsepgfromrep  5250  fununmo  6607  funcnvsn  6612  nfunsn  6947  caovmo  7682  iunmapdisj  10129  brdom3  10634  brdom5  10635  brdom4  10636  nqerf  11042  shftfn  15255  2ndcdisj2  23806  plyexmo  26666  ajfuni  31491  funadj  32518  cnlnadjeui  32709  amosym1  37392  sinnpoly  48146  funressnvmo  48320