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

Theorem mobidv 2549
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 1927 . 2 (𝜑 → ∀𝑥(𝜓𝜒))
3 mobi 2547 . 2 (∀𝑥(𝜓𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
42, 3syl 17 1 (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538  ∃*wmo 2538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-mo 2540
This theorem is referenced by:  moanimv  2619  rmobidva  3395  rmoeq1OLD  3418  mosubopt  5515  dffun6f  6579  funmo  6581  funmoOLD  6582  caovmo  7670  1stconst  8125  2ndconst  8126  brdom3  10568  brdom6disj  10572  imasaddfnlem  17573  imasvscafn  17582  hausflim  23989  hausflf  24005  cnextfun  24072  haustsms  24144  limcmo  25917  perfdvf  25938  rmounid  32514  rmoeqbidv  36214  disjeq12dv  36216  phpreu  37611  alrmomodm  38360  funressnfv  47055  funressnmo  47058  mosn  48732  mof02  48748  mofsn2  48754  f1omo  48792  isthinc  49069  isthincd2lem1  49075  thincmoALT  49078  thincmod  49079  isthincd  49085  thincpropd  49091  setcthin  49112
  Copyright terms: Public domain W3C validator