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

Theorem moim 2517
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 1741 . . 3 (∀𝑥(𝜑𝜓) → (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
32eximdv 1844 . 2 (∀𝑥(𝜑𝜓) → (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
4 mo2v 2475 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
5 mo2v 2475 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
63, 4, 53imtr4g 285 1 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479  wex 1702  ∃*wmo 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-10 2017  ax-12 2045
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1703  df-nf 1708  df-eu 2472  df-mo 2473
This theorem is referenced by:  moimi  2518  euimmo  2520  moexex  2539  rmoim  3401  rmoimi2  3403  disjss1  4617  disjss3  4643  reusv1OLD  4858  funmo  5892  brdom6disj  9339  uptx  21409  taylf  24096  moimd  29298  ssrmo  29306  funressnfv  40971
  Copyright terms: Public domain W3C validator