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

Theorem moimi 2625
Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1904. (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 1805 . . 3 (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
43eximi 1828 . 2 (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
5 df-mo 2620 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
6 df-mo 2620 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
74, 5, 63imtr4i 293 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1528  wex 1773  ∃*wmo 2618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ex 1774  df-mo 2620
This theorem is referenced by:  mobii  2629  moa1  2633  moan  2634  moor  2636  mooran1  2637  mooran2  2638  moaneu  2707  2moexv  2711  2euexv  2715  2exeuv  2716  2moex  2724  2euex  2725  2exeu  2730  sndisj  5054  disjxsn  5056  axsepgfromrep  5198  fununmo  6398  funcnvsn  6401  nfunsn  6704  caovmo  7375  iunmapdisj  9438  brdom3  9939  brdom5  9940  brdom4  9941  nqerf  10341  shftfn  14422  2ndcdisj2  21981  plyexmo  24817  ajfuni  28550  funadj  29577  cnlnadjeui  29768  funressnvmo  43146
  Copyright terms: Public domain W3C validator