Theorem rmov

Description: An at-most-one quantifier restricted to the universe is unrestricted. (Contributed by Alexander van der Vekens, 17-Jun-2017)

	Ref	Expression
Assertion	rmov	$$⊢{\exists }^{*}x\in \mathrm{V}\phi \leftrightarrow {\exists }^{*}x\phi$$

Proof

Step	Hyp	Ref	Expression
1		df-rmo	$$⊢{\exists }^{*}x\in \mathrm{V}\phi \leftrightarrow {\exists }^{*}x\left(x\in \mathrm{V}\wedge \phi \right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	biantrur	$$⊢\phi \leftrightarrow \left(x\in \mathrm{V}\wedge \phi \right)$$
4	3	mobii	$$⊢{\exists }^{*}x\phi \leftrightarrow {\exists }^{*}x\left(x\in \mathrm{V}\wedge \phi \right)$$
5	1 4	bitr4i	$$⊢{\exists }^{*}x\in \mathrm{V}\phi \leftrightarrow {\exists }^{*}x\phi$$