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	⊢ ( ∃* 𝑥 ∈ V 𝜑 ↔ ∃* 𝑥 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-rmo	⊢ ( ∃* 𝑥 ∈ V 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ V ∧ 𝜑 ) )
2		vex	⊢ 𝑥 ∈ V
3	2	biantrur	⊢ ( 𝜑 ↔ ( 𝑥 ∈ V ∧ 𝜑 ) )
4	3	mobii	⊢ ( ∃* 𝑥 𝜑 ↔ ∃* 𝑥 ( 𝑥 ∈ V ∧ 𝜑 ) )
5	1 4	bitr4i	⊢ ( ∃* 𝑥 ∈ V 𝜑 ↔ ∃* 𝑥 𝜑 )