Theorem rmo0

Description: Vacuous restricted at-most-one quantifier is always true. (Contributed by AV, 3-Apr-2023)

	Ref	Expression
Assertion	rmo0	$$⊢{\exists }^{*}x\in \varnothing \phi$$

Proof

Step	Hyp	Ref	Expression
1		rex0	$$⊢\neg \exists x\in \varnothing \phi$$
2	1	pm2.21i	$$⊢\exists x\in \varnothing \phi \to \exists !x\in \varnothing \phi$$
3		rmo5	$$⊢{\exists }^{*}x\in \varnothing \phi \leftrightarrow \left(\exists x\in \varnothing \phi \to \exists !x\in \varnothing \phi \right)$$
4	2 3	mpbir	$$⊢{\exists }^{*}x\in \varnothing \phi$$