Metamath Proof Explorer


Theorem nfreu1

Description: The setvar x is not free in E! x e. A ph . (Contributed by NM, 19-Mar-1997)

Ref Expression
Assertion nfreu1 𝑥 ∃! 𝑥𝐴 𝜑

Proof

Step Hyp Ref Expression
1 df-reu ( ∃! 𝑥𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥𝐴𝜑 ) )
2 nfeu1 𝑥 ∃! 𝑥 ( 𝑥𝐴𝜑 )
3 1 2 nfxfr 𝑥 ∃! 𝑥𝐴 𝜑