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

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.
StepHypRef Expression
1 moimi.1 . . . . 5 (𝜑𝜓)
21imim1i 63 . . . 4 ((𝜓𝑥 = 𝑦) → (𝜑𝑥 = 𝑦))
32alimi 1813 . . 3 (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
43eximi 1836 . 2 (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
5 df-mo 2557 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
6 df-mo 2557 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
74, 5, 63imtr4i 295 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator