Theorem mobidv 2633

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

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1535  ∃*wmo 2620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-mo 2622

This theorem is referenced by:  moanimv  2704  rmoeq1  3408  mosubopt  5400  dffun6f  6369  funmo  6371  caovmo  7385  1stconst  7795  2ndconst  7796  brdom3  9950  brdom6disj  9954  imasaddfnlem  16801  imasvscafn  16810  hausflim  22589  hausflf  22605  cnextfun  22672  haustsms  22744  limcmo  24480  perfdvf  24501  rmounid  30259  phpreu  34891  alrmomodm  35628  funressnfv  43298  funressnmo  43301