Theorem rmosn

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

	Ref	Expression
Assertion	rmosn	$$⊢{\exists }^{*}x\in \left\{A\right\}\phi$$

Proof

Step	Hyp	Ref	Expression
1		idd	$$⊢A\in \mathrm{V}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
2		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
3		sbceq1a	$$⊢x=A\to \left(\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
4	2 3	rexsngf	$$⊢A\in \mathrm{V}\to \left(\exists x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
5	2 3	reusngf	$$⊢A\in \mathrm{V}\to \left(\exists !x\in \left\{A\right\}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
6	1 4 5	3imtr4d	$$⊢A\in \mathrm{V}\to \left(\exists x\in \left\{A\right\}\phi \to \exists !x\in \left\{A\right\}\phi \right)$$
7		rmo5	$$⊢{\exists }^{*}x\in \left\{A\right\}\phi \leftrightarrow \left(\exists x\in \left\{A\right\}\phi \to \exists !x\in \left\{A\right\}\phi \right)$$
8	6 7	sylibr	$$⊢A\in \mathrm{V}\to {\exists }^{*}x\in \left\{A\right\}\phi$$
9		rmo0	$$⊢{\exists }^{*}x\in \varnothing \phi$$
10		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
11		rmoeq1	$$⊢\left\{A\right\}=\varnothing \to \left({\exists }^{*}x\in \left\{A\right\}\phi \leftrightarrow {\exists }^{*}x\in \varnothing \phi \right)$$
12	10 11	sylbi	$$⊢\neg A\in \mathrm{V}\to \left({\exists }^{*}x\in \left\{A\right\}\phi \leftrightarrow {\exists }^{*}x\in \varnothing \phi \right)$$
13	9 12	mpbiri	$$⊢\neg A\in \mathrm{V}\to {\exists }^{*}x\in \left\{A\right\}\phi$$
14	8 13	pm2.61i	$$⊢{\exists }^{*}x\in \left\{A\right\}\phi$$