Theorem moimi 2545

Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1913. (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 1814	. . 3 ⊢ (∀𝑥(𝜓 → 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	3	eximi 1837	. 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
5		df-mo 2540	. 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦))
6		df-mo 2540	. 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
7	4, 5, 6	3imtr4i 292	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

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

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

This theorem depends on definitions:  df-bi 206  df-ex 1783  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  5065  disjxsn  5067  axsepgfromrep  5221  fununmo  6481  funcnvsn  6484  nfunsn  6811  caovmo  7509  iunmapdisj  9779  brdom3  10284  brdom5  10285  brdom4  10286  nqerf  10686  shftfn  14784  2ndcdisj2  22608  plyexmo  25473  ajfuni  29221  funadj  30248  cnlnadjeui  30439  funressnvmo  44539