Theorem moimi 2545

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1914. (Revised by Steven Nguyen, 9-May-2023.)

Hypothesis

Ref	Expression
moimi.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
moimi	⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

Proof of Theorem moimi

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		moimi.1	. . . . 5 ⊢ (𝜑 → 𝜓)
2	1	imim1i 63	. . . 4 ⊢ ((𝜓 → 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
3	2	alimi 1815	. . 3 ⊢ (∀𝑥(𝜓 → 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	3	eximi 1838	. 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
5		df-mo 2540	. 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦))
6		df-mo 2540	. 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
7	4, 5, 6	3imtr4i 291	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1537  ∃wex 1783  ∃*wmo 2538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813

This theorem depends on definitions:  df-bi 206  df-ex 1784  df-mo 2540

This theorem is referenced by:  mobii  2548  moa1  2551  moan  2552  moor  2554  mooran1  2555  mooran2  2556  moaneu  2625  2moexv  2629  2euexv  2633  2exeuv  2634  2moex  2642  2euex  2643  2exeu  2648  sndisj  5061  disjxsn  5063  axsepgfromrep  5216  fununmo  6465  funcnvsn  6468  nfunsn  6793  caovmo  7487  iunmapdisj  9710  brdom3  10215  brdom5  10216  brdom4  10217  nqerf  10617  shftfn  14712  2ndcdisj2  22516  plyexmo  25378  ajfuni  29122  funadj  30149  cnlnadjeui  30340  funressnvmo  44426