alsanmo

Description: An "all some" statement conjoined with the claim that at most one x satisfies its antecedent is equivalent to the universal part conjoined with the claim that exactly one x satisfies the antecedent. The "all some" quantifier supplies the existence of such an x and E* x ph supplies the at-most-one part, so together they yield E! x ph . (Contributed by Peter Mazsa and David A. Wheeler, 20-Jul-2026)

		Ref	Expression
	Assertion	alsanmo	$⊢ (\forall\exists x (φ \to ψ) \land \exists^{*} x φ) \leftrightarrow (\forall x (φ \to ψ) \land \exists! x φ)$

Proof

Step	Hyp	Ref	Expression
1		df-als	$⊢ \forall\exists x (φ \to ψ) \leftrightarrow (\forall x (φ \to ψ) \land \exists x φ)$
2	1	anbi1i	$⊢ (\forall\exists x (φ \to ψ) \land \exists^{} x φ) \leftrightarrow ((\forall x (φ \to ψ) \land \exists x φ) \land \exists^{} x φ)$
3		anass	$⊢ ((\forall x (φ \to ψ) \land \exists x φ) \land \exists^{} x φ) \leftrightarrow (\forall x (φ \to ψ) \land (\exists x φ \land \exists^{} x φ))$
4		df-eu	$⊢ \exists! x φ \leftrightarrow (\exists x φ \land \exists^{*} x φ)$
5	4	bicomi	$⊢ (\exists x φ \land \exists^{*} x φ) \leftrightarrow \exists! x φ$
6	5	anbi2i	$⊢ (\forall x (φ \to ψ) \land (\exists x φ \land \exists^{*} x φ)) \leftrightarrow (\forall x (φ \to ψ) \land \exists! x φ)$
7	2 3 6	3bitri	$⊢ (\forall\exists x (φ \to ψ) \land \exists^{*} x φ) \leftrightarrow (\forall x (φ \to ψ) \land \exists! x φ)$

Metamath Proof Explorer

Theorem alsanmo

Proof