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

Theorem mobidv 2543
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 1930 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 mobi 2541 . 2 (∀𝑥(𝜓𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1539  ∃*wmo 2532
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 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-mo 2534
This theorem is referenced by:  moanimv  2615  rmobidva  3391  rmoeq1OLD  3416  mosubopt  5509  dffun6f  6558  funmo  6560  funmoOLD  6561  caovmo  7640  1stconst  8082  2ndconst  8083  brdom3  10519  brdom6disj  10523  imasaddfnlem  17470  imasvscafn  17479  hausflim  23476  hausflf  23492  cnextfun  23559  haustsms  23631  limcmo  25390  perfdvf  25411  rmounid  31722  phpreu  36460  alrmomodm  37216  funressnfv  45739  funressnmo  45742  mosn  47450  mof02  47458  mofsn2  47464  f1omo  47480  isthinc  47594  isthincd2lem1  47600  thincmoALT  47603  thincmod  47604  isthincd  47610  setcthin  47628
  Copyright terms: Public domain W3C validator