Theorem ralsanmo

Description: An "all some" statement restricted to a class, conjoined with the claim that at most one x in A satisfies its antecedent, is equivalent to the universal part conjoined with the claim that exactly one x in A satisfies the antecedent. This is the restricted counterpart of alsanmo . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

	Ref	Expression
Assertion	ralsanmo	⊢ ( ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		df-rals	⊢ ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) )
2	1	anbi1i	⊢ ( ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) )
3		anass	⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜑 ) ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ) )
4		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) )
5	4	bicomi	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ∃! 𝑥 ∈ 𝐴 𝜑 )
6	5	anbi2i	⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ( ∃ 𝑥 ∈ 𝐴 𝜑 ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) )
7	2 3 6	3bitri	⊢ ( ( ∀∃ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 𝜑 ) ↔ ( ∀ 𝑥 ∈ 𝐴 ( 𝜑 → 𝜓 ) ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) )