Theorem mobidv 2547

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

Step	Hyp	Ref	Expression
1		mobidv.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	alrimiv 1925	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		mobi 2545	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	2, 3	syl 17	1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535  ∃*wmo 2536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-mo 2538

This theorem is referenced by:  moanimv  2617  rmobidva  3393  rmoeq1OLD  3416  mosubopt  5520  dffun6f  6581  funmo  6583  funmoOLD  6584  caovmo  7670  1stconst  8124  2ndconst  8125  brdom3  10566  brdom6disj  10570  imasaddfnlem  17575  imasvscafn  17584  hausflim  24005  hausflf  24021  cnextfun  24088  haustsms  24160  limcmo  25932  perfdvf  25953  rmounid  32523  rmoeqbidv  36195  disjeq12dv  36198  phpreu  37591  alrmomodm  38341  funressnfv  46993  funressnmo  46996  mosn  48661  mof02  48669  mofsn2  48675  f1omo  48691  isthinc  48821  isthincd2lem1  48827  thincmoALT  48830  thincmod  48831  isthincd  48837  setcthin  48856