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

Theorem mobidv 2564
Description: Formula-building rule for the at-most-one quantifier (deduction form). (Contributed by Mario Carneiro, 7-Oct-2016.) Reduce axiom dependencies and shorten proof. (Revised by BJ, 7-Oct-2022.)
Hypothesis
Ref Expression
mobidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mobidv (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem mobidv
StepHypRef Expression
1 mobidv.1 . . 3 (𝜑 → (𝜓𝜒))
21alrimiv 1970 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 mobi 2560 . 2 (∀𝑥(𝜓𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1599  ∃*wmo 2549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-mo 2551
This theorem is referenced by:  moanimv  2654  rmoeq1  3333  mosubopt  5207  dffun6f  6149  funmo  6151  caovmo  7148  1stconst  7546  2ndconst  7547  brdom3  9685  brdom6disj  9689  imasaddfnlem  16574  imasvscafn  16583  hausflim  22193  hausflf  22209  cnextfun  22276  haustsms  22347  limcmo  24083  perfdvf  24104  phpreu  34018  alrmomodm  34752  funressnfv  42107  funressnmo  42111
  Copyright terms: Public domain W3C validator