Theorem mobidv 2583

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

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1565  ∃*wmo 2571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-mo 2573

This theorem is referenced by:  moanimv  2653  rmobidva  3389  mosubopt  5496  dffun6f  6554  funmo  6555  caovmo  7650  1stconst  8097  2ndconst  8098  brdom3  10514  brdom6disj  10518  imasaddfnlem  17584  imasvscafn  17593  hausflim  24109  hausflf  24125  cnextfun  24192  haustsms  24264  limcmo  26012  perfdvf  26033  rmounid  32784  rmoeqbidv  36650  disjeq12dv  36652  phpreu  38180  alrmomodm  38935  funressnfv  47706  funressnmo  47709  mosn  49513  mof02  49539  mofsn2  49545  f1omo  49593  f1omoOLD  49594  isthinc  50119  isthincd2lem1  50125  thincmoALT  50129  thincmod  50130  isthincd  50136  thincpropd  50142  indcthing  50160  discthing  50161  setcthin  50165