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

Theorem mobidv 2479
 Description: Formula-building rule for "at most one" quantifier (deduction rule). (Contributed by Mario Carneiro, 7-Oct-2016.)
Hypothesis
Ref Expression
mobidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
mobidv (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)

Proof of Theorem mobidv
StepHypRef Expression
1 nfv 1830 . 2 𝑥𝜑
2 mobidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mobid 2477 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195  ∃*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-12 2034 This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-eu 2462  df-mo 2463 This theorem is referenced by:  mobii  2481  mosubopt  4897  dffun6f  5818  funmo  5820  caovmo  6769  1stconst  7152  2ndconst  7153  brdom3  9231  brdom6disj  9235  imasaddfnlem  16011  imasvscafn  16020  hausflim  21595  hausflf  21611  cnextfun  21678  haustsms  21749  limcmo  23452  perfdvf  23473  phpreu  32563  funressnfv  39857
 Copyright terms: Public domain W3C validator