Theorem mobidv 2564

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

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1599  ∃*wmo 2549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-mo 2551

This theorem is referenced by:  moanimv  2654  rmoeq1  3333  mosubopt  5207  dffun6f  6149  funmo  6151  caovmo  7148  1stconst  7546  2ndconst  7547  brdom3  9685  brdom6disj  9689  imasaddfnlem  16574  imasvscafn  16583  hausflim  22193  hausflf  22209  cnextfun  22276  haustsms  22347  limcmo  24083  perfdvf  24104  phpreu  34018  alrmomodm  34752  funressnfv  42107  funressnmo  42111