Theorem moimi 2562

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 1813	. . 3 ⊢ (∀𝑥(𝜓 → 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
4	3	eximi 1836	. 2 ⊢ (∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
5		df-mo 2557	. 2 ⊢ (∃*𝑥𝜓 ↔ ∃𝑦∀𝑥(𝜓 → 𝑥 = 𝑦))
6		df-mo 2557	. 2 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
7	4, 5, 6	3imtr4i 295	1 ⊢ (∃*𝑥𝜓 → ∃*𝑥𝜑)

Syntax hints:   → wi 4  ∀wal 1536  ∃wex 1781  ∃*wmo 2555

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

This theorem depends on definitions:  df-bi 210  df-ex 1782  df-mo 2557

This theorem is referenced by:  mobii  2565  moa1  2569  moan  2570  moor  2572  mooran1  2573  mooran2  2574  moaneu  2644  2moexv  2648  2euexv  2652  2exeuv  2653  2moex  2661  2euex  2662  2exeu  2667  sndisj  5027  disjxsn  5029  axsepgfromrep  5171  fununmo  6387  funcnvsn  6390  nfunsn  6700  caovmo  7387  iunmapdisj  9496  brdom3  10001  brdom5  10002  brdom4  10003  nqerf  10403  shftfn  14493  2ndcdisj2  22170  plyexmo  25021  ajfuni  28754  funadj  29781  cnlnadjeui  29972  funressnvmo  44038