Theorem moimi 2538

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

Syntax hints:   → wi 4  ∀wal 1538  ∃wex 1779  ∃*wmo 2531

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

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-mo 2533

This theorem is referenced by:  mobii  2541  moa1  2544  moan  2545  moor  2547  mooran1  2548  mooran2  2549  moaneu  2616  2moexv  2620  2euexv  2624  2exeuv  2625  2moex  2633  2euex  2634  2exeu  2639  sndisj  5099  disjxsn  5101  axsepgfromrep  5249  fununmo  6563  funcnvsn  6566  nfunsn  6900  caovmo  7626  iunmapdisj  9976  brdom3  10481  brdom5  10482  brdom4  10483  nqerf  10883  shftfn  15039  2ndcdisj2  23344  plyexmo  26221  ajfuni  30788  funadj  31815  cnlnadjeui  32006  amosym1  36414  sinnpoly  46892  funressnvmo  47046