Theorem alseud

Description: Introduction rule: "all some one" holds if the "for all" part holds and the antecedent has exactly one witness. This is the converse of alseu1d and alseu2d taken together. (Contributed by David A. Wheeler, 21-Jul-2026)

	Ref	Expression
Hypotheses	alseud.1	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
	alseud.2	⊢ ( 𝜑 → ∃! 𝑥 𝜓 )
Assertion	alseud	⊢ ( 𝜑 → ∀∃! 𝑥 ( 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		alseud.1	⊢ ( 𝜑 → ∀ 𝑥 ( 𝜓 → 𝜒 ) )
2		alseud.2	⊢ ( 𝜑 → ∃! 𝑥 𝜓 )
3		df-alseu	⊢ ( ∀∃! 𝑥 ( 𝜓 → 𝜒 ) ↔ ( ∀ 𝑥 ( 𝜓 → 𝜒 ) ∧ ∃! 𝑥 𝜓 ) )
4	1 2 3	sylanbrc	⊢ ( 𝜑 → ∀∃! 𝑥 ( 𝜓 → 𝜒 ) )