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

Theorem moimi 2545
Description: The at-most-one quantifier reverses implication. (Contributed by NM, 15-Feb-2006.) Remove use of ax-5 1910. (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 1811 . . 3 (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦))
43eximi 1835 . 2 (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦))
5 df-mo 2540 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
6 df-mo 2540 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
74, 5, 63imtr4i 292 1 (∃*𝑥𝜓 → ∃*𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1538  wex 1779  ∃*wmo 2538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ex 1780  df-mo 2540
This theorem is referenced by:  mobii  2548  moa1  2551  moan  2552  moor  2554  mooran1  2555  mooran2  2556  moaneu  2623  2moexv  2627  2euexv  2631  2exeuv  2632  2moex  2640  2euex  2641  2exeu  2646  sndisj  5135  disjxsn  5137  axsepgfromrep  5294  fununmo  6613  funcnvsn  6616  nfunsn  6948  caovmo  7670  iunmapdisj  10063  brdom3  10568  brdom5  10569  brdom4  10570  nqerf  10970  shftfn  15112  2ndcdisj2  23465  plyexmo  26355  ajfuni  30878  funadj  31905  cnlnadjeui  32096  amosym1  36427  funressnvmo  47057
  Copyright terms: Public domain W3C validator