MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  moimi Structured version   Visualization version   GIF version

Theorem moimi 2543
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.
StepHypRef Expression
1 moimi.1 . . . . 5 (𝜑𝜓)
21imim1i 63 . . . 4 ((𝜓𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
32alimi 1813 . . 3 (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
43eximi 1837 . 2 (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
5 df-mo 2538 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
6 df-mo 2538 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
74, 5, 63imtr4i 291 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1539  wex 1781  ∃*wmo 2536
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 206  df-ex 1782  df-mo 2538
This theorem is referenced by:  mobii  2546  moa1  2549  moan  2550  moor  2552  mooran1  2553  mooran2  2554  moaneu  2623  2moexv  2627  2euexv  2631  2exeuv  2632  2moex  2640  2euex  2641  2exeu  2646  sndisj  5094  disjxsn  5096  axsepgfromrep  5252  fununmo  6545  funcnvsn  6548  nfunsn  6881  caovmo  7585  iunmapdisj  9917  brdom3  10422  brdom5  10423  brdom4  10424  nqerf  10824  shftfn  14912  2ndcdisj2  22754  plyexmo  25619  ajfuni  29646  funadj  30673  cnlnadjeui  30864  amosym1  34830  funressnvmo  45174
  Copyright terms: Public domain W3C validator