Theorem mobidv

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)

	Ref	Expression
Hypothesis	mobidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
Assertion	mobidv	⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		mobidv.1	⊢ ( 𝜑 → ( 𝜓 ↔ 𝜒 ) )
2	1	alrimiv	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 ↔ 𝜒 ) )
3		mobi	⊢ ( ∀ 𝑥 ( 𝜓 ↔ 𝜒 ) → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 𝜒 ) )
4	2 3	syl	⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑥 𝜒 ) )