Metamath Proof Explorer


Theorem reuv

Description: A unique existential quantifier restricted to the universe is unrestricted. (Contributed by NM, 1-Nov-2010)

Ref Expression
Assertion reuv ∃!xVφ∃!xφ

Proof

Step Hyp Ref Expression
1 df-reu ∃!xVφ∃!xxVφ
2 vex xV
3 2 biantrur φxVφ
4 3 eubii ∃!xφ∃!xxVφ
5 1 4 bitr4i ∃!xVφ∃!xφ