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

Theorem moim 2507
 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 81 . . . 4 ((𝜑𝜓) → ((𝜓𝑥 = 𝑦) → (𝜑𝑥 = 𝑦)))
21al2imi 1733 . . 3 (∀𝑥(𝜑𝜓) → (∀𝑥(𝜓𝑥 = 𝑦) → ∀𝑥(𝜑𝑥 = 𝑦)))
32eximdv 1833 . 2 (∀𝑥(𝜑𝜓) → (∃𝑦𝑥(𝜓𝑥 = 𝑦) → ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
4 mo2v 2465 . 2 (∃*𝑥𝜓 ↔ ∃𝑦𝑥(𝜓𝑥 = 𝑦))
5 mo2v 2465 . 2 (∃*𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
63, 4, 53imtr4g 284 1 (∀𝑥(𝜑𝜓) → (∃*𝑥𝜓 → ∃*𝑥𝜑))
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1473  ∃wex 1695  ∃*wmo 2459 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-12 2034 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463 This theorem is referenced by:  moimi  2508  euimmo  2510  moexex  2529  rmoim  3374  rmoimi2  3376  disjss1  4559  disjss3  4582  reusv1OLD  4793  funmo  5820  brdom6disj  9235  uptx  21238  taylf  23919  moimd  28710  ssrmo  28718  funressnfv  39857
 Copyright terms: Public domain W3C validator