Theorem mobidv 2579

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 1950	. 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒))
3		mobi 2577	. 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))
4	2, 3	syl 18	1 ⊢ (𝜑 → (∃*𝑥𝜓 ↔ ∃*𝑥𝜒))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1561  ∃*wmo 2567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-mo 2569

This theorem is referenced by:  moanimv  2649  rmobidva  3383  mosubopt  5484  dffun6f  6540  funmo  6541  caovmo  7637  1stconst  8083  2ndconst  8084  brdom3  10500  brdom6disj  10504  imasaddfnlem  17572  imasvscafn  17581  hausflim  24099  hausflf  24115  cnextfun  24182  haustsms  24254  limcmo  26002  perfdvf  26023  rmounid  32751  rmoeqbidv  36586  disjeq12dv  36588  phpreu  38115  alrmomodm  38870  funressnfv  47635  funressnmo  47638  mosn  49442  mof02  49468  mofsn2  49474  f1omo  49522  f1omoOLD  49523  isthinc  50048  isthincd2lem1  50054  thincmoALT  50058  thincmod  50059  isthincd  50065  thincpropd  50071  indcthing  50089  discthing  50090  setcthin  50094