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

Theorem mobidv 2611
 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 1928 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 mobi 2608 . 2 (∀𝑥(𝜓𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1536  ∃*wmo 2599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-mo 2601 This theorem is referenced by:  moanimv  2684  rmoeq1  3364  mosubopt  5368  dffun6f  6342  funmo  6344  caovmo  7369  1stconst  7782  2ndconst  7783  brdom3  9943  brdom6disj  9947  imasaddfnlem  16796  imasvscafn  16805  hausflim  22589  hausflf  22605  cnextfun  22672  haustsms  22744  limcmo  24488  perfdvf  24509  rmounid  30269  phpreu  35034  alrmomodm  35766  funressnfv  43622  funressnmo  43625
 Copyright terms: Public domain W3C validator