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

Theorem moim 2548
 Description: "At most one" reverses implication. (Contributed by NM, 22-Apr-1995.)
Assertion
Ref Expression
moim (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))

Proof of Theorem moim
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 imim1 83 . . . 4 ((𝜑𝜓) → ((𝜓𝑥 = 𝑦) → (𝜑𝑥 = 𝑦)))
21al2imi 1783 . . 3 (∀𝑥(𝜑𝜓) → (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
32eximdv 1886 . 2 (∀𝑥(𝜑𝜓) → (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
4 mo2v 2505 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
5 mo2v 2505 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
63, 4, 53imtr4g 285 1 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521  ∃wex 1744  ∃*wmo 2499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-12 2087 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750  df-eu 2502  df-mo 2503 This theorem is referenced by:  moimi  2549  euimmo  2551  moexex  2570  rmoim  3440  rmoimi2  3442  disjss1  4658  disjss3  4684  reusv1OLD  4897  funmo  5942  brdom6disj  9392  uptx  21476  taylf  24160  moimd  29454  ssrmo  29461  funressnfv  41529
 Copyright terms: Public domain W3C validator