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

Theorem moimi 2540
Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1914. (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 1814 . . 3 (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
43eximi 1838 . 2 (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
5 df-mo 2535 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
6 df-mo 2535 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
74, 5, 63imtr4i 292 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wex 1782  ∃*wmo 2533
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 2535
This theorem is referenced by:  mobii  2543  moa1  2546  moan  2547  moor  2549  mooran1  2550  mooran2  2551  moaneu  2620  2moexv  2624  2euexv  2628  2exeuv  2629  2moex  2637  2euex  2638  2exeu  2643  sndisj  5140  disjxsn  5142  axsepgfromrep  5298  fununmo  6596  funcnvsn  6599  nfunsn  6934  caovmo  7644  iunmapdisj  10018  brdom3  10523  brdom5  10524  brdom4  10525  nqerf  10925  shftfn  15020  2ndcdisj2  22961  plyexmo  25826  ajfuni  30112  funadj  31139  cnlnadjeui  31330  amosym1  35311  funressnvmo  45755
  Copyright terms: Public domain W3C validator