Metamath Proof Explorer


Theorem nfeuw

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

Ref Expression
Hypothesis nfeuw.1 x φ
Assertion nfeuw x ∃! y φ

Proof

Step Hyp Ref Expression
1 nfeuw.1 x φ
2 nftru y
3 1 a1i x φ
4 2 3 nfeudw x ∃! y φ
5 4 mptru x ∃! y φ