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

Theorem mobidv 2519
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 1883 . 2 𝑥𝜑
2 mobidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mobid 2517 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  ∃*wmo 2499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-eu 2502  df-mo 2503
This theorem is referenced by:  mobii  2521  mosubopt  5001  dffun6f  5940  funmo  5942  caovmo  6913  1stconst  7310  2ndconst  7311  brdom3  9388  brdom6disj  9392  imasaddfnlem  16235  imasvscafn  16244  hausflim  21832  hausflf  21848  cnextfun  21915  haustsms  21986  limcmo  23691  perfdvf  23712  phpreu  33523  alrmomodm  34264  funressnfv  41529
  Copyright terms: Public domain W3C validator