Metamath Proof Explorer

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 
|- ( E* x e. _V ph <-> E* x ph )

Proof

Step Hyp Ref Expression
1 df-rmo 
 |-  ( E* x e. _V ph <-> E* x ( x e. _V /\ ph ) )
2 vex 
 |-  x e. _V
3 2 biantrur 
 |-  ( ph <-> ( x e. _V /\ ph ) )
4 3 mobii 
 |-  ( E* x ph <-> E* x ( x e. _V /\ ph ) )
5 1 4 bitr4i 
 |-  ( E* x e. _V ph <-> E* x ph )