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

Theorem mobidv 2561
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 1886 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 mobi 2556 . 2 (∀𝑥(𝜓𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wal 1505  ∃*wmo 2545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869
This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-mo 2547
This theorem is referenced by:  moanimv  2653  rmoeq1  3342  mosubopt  5250  dffun6f  6196  funmo  6198  caovmo  7195  1stconst  7597  2ndconst  7598  brdom3  9742  brdom6disj  9746  imasaddfnlem  16651  imasvscafn  16660  hausflim  22287  hausflf  22303  cnextfun  22370  haustsms  22441  limcmo  24177  perfdvf  24198  phpreu  34317  alrmomodm  35059  funressnfv  42683  funressnmo  42687
  Copyright terms: Public domain W3C validator