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

Theorem mobidv 2490
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 1840 . 2 𝑥𝜑
2 mobidv.1 . 2 (𝜑 → (𝜓𝜒))
31, 2mobid 2488 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  ∃*wmo 2470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-ex 1702  df-nf 1707  df-eu 2473  df-mo 2474
This theorem is referenced by:  mobii  2492  mosubopt  4937  dffun6f  5866  funmo  5868  caovmo  6831  1stconst  7217  2ndconst  7218  brdom3  9302  brdom6disj  9306  imasaddfnlem  16120  imasvscafn  16129  hausflim  21708  hausflf  21724  cnextfun  21791  haustsms  21862  limcmo  23569  perfdvf  23590  phpreu  33060  funressnfv  40538
  Copyright terms: Public domain W3C validator