Theorem mobidv 2577

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568  ∃*wmo 2565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-mo 2567

This theorem is referenced by:  moanimv  2647  rmobidva  3382  mosubopt  5495  dffun6f  6553  funmo  6554  caovmo  7649  1stconst  8096  2ndconst  8097  brdom3  10513  brdom6disj  10517  imasaddfnlem  17583  imasvscafn  17592  hausflim  24119  hausflf  24135  cnextfun  24202  haustsms  24274  limcmo  26022  perfdvf  26043  rmounid  32819  rmoeqbidv  36703  disjeq12dv  36705  phpreu  38233  alrmomodm  38986  funressnfv  47757  funressnmo  47760  mosn  49568  mof02  49594  mofsn2  49600  f1omo  49648  f1omoOLD  49649  isthinc  50174  isthincd2lem1  50180  thincmoALT  50184  thincmod  50185  isthincd  50191  thincpropd  50197  indcthing  50215  discthing  50216  setcthin  50220