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	|- F/ y ph
	nfeudw.2	|- ( ph -> F/ x ps )
Assertion	nfeudw	|- ( ph -> F/ x E! y ps )

Proof

Step	Hyp	Ref	Expression
1		nfeudw.1	|- F/ y ph
2		nfeudw.2	|- ( ph -> F/ x ps )
3		df-eu	|- ( E! y ps <-> ( E. y ps /\ E* y ps ) )
4	1 2	nfexd	|- ( ph -> F/ x E. y ps )
5	1 2	nfmodv	|- ( ph -> F/ x E* y ps )
6	4 5	nfand	|- ( ph -> F/ x ( E. y ps /\ E* y ps ) )
7	3 6	nfxfrd	|- ( ph -> F/ x E! y ps )