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

Proof

Step Hyp Ref Expression
1 df-reu ( ∃! 𝑥 ∈ V 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ V ∧ 𝜑 ) )
2 vex 𝑥 ∈ V
3 2 biantrur ( 𝜑 ↔ ( 𝑥 ∈ V ∧ 𝜑 ) )
4 3 eubii ( ∃! 𝑥 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ V ∧ 𝜑 ) )
5 1 4 bitr4i ( ∃! 𝑥 ∈ V 𝜑 ↔ ∃! 𝑥 𝜑 )