Description: The setvar x is not free in E! x e. A ph . (Contributed by NM, 19-Mar-1997)
Ref | Expression | ||
---|---|---|---|
Assertion | nfreu1 | ⊢ Ⅎ 𝑥 ∃! 𝑥 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-reu | ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 ↔ ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) | |
2 | nfeu1 | ⊢ Ⅎ 𝑥 ∃! 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) | |
3 | 1 2 | nfxfr | ⊢ Ⅎ 𝑥 ∃! 𝑥 ∈ 𝐴 𝜑 |