Metamath Proof Explorer

Theorem nfeudw

Description: Bound-variable hypothesis builder for the unique existential quantifier. Deduction version of nfeu . Version of nfeud with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Gino Giotto, 10-Jan-2024)

Ref Expression
Hypotheses nfeudw.1 y φ
nfeudw.2 φ x ψ
Assertion nfeudw φ x ∃! y ψ


Step Hyp Ref Expression
1 nfeudw.1 y φ
2 nfeudw.2 φ x ψ
3 df-eu ∃! y ψ y ψ * y ψ
4 1 2 nfexd φ x y ψ
5 1 2 nfmodv φ x * y ψ
6 4 5 nfand φ x y ψ * y ψ
7 3 6 nfxfrd φ x ∃! y ψ