Theorem moimi 2540

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

Syntax hints:   → wi 4  ∀wal 1539  ∃wex 1780  ∃*wmo 2533

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

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-mo 2535

This theorem is referenced by:  mobii  2543  moa1  2546  moan  2547  moor  2549  mooran1  2550  mooran2  2551  moaneu  2618  2moexv  2622  2euexv  2626  2exeuv  2627  2moex  2635  2euex  2636  2exeu  2641  sndisj  5083  disjxsn  5085  axsepgfromrep  5232  fununmo  6528  funcnvsn  6531  nfunsn  6861  caovmo  7583  iunmapdisj  9911  brdom3  10416  brdom5  10417  brdom4  10418  nqerf  10818  shftfn  14977  2ndcdisj2  23370  plyexmo  26246  ajfuni  30834  funadj  31861  cnlnadjeui  32052  amosym1  36459  sinnpoly  46921  funressnvmo  47075