Theorem nrexdv

Description: Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003) (Proof shortened by Wolf Lammen, 5-Jan-2020)

	Ref	Expression
Hypothesis	nrexdv.1	|- ( ( ph /\ x e. A ) -> -. ps )
Assertion	nrexdv	|- ( ph -> -. E. x e. A ps )

Proof

Step	Hyp	Ref	Expression
1		nrexdv.1	|- ( ( ph /\ x e. A ) -> -. ps )
2	1	ralrimiva	|- ( ph -> A. x e. A -. ps )
3		ralnex	|- ( A. x e. A -. ps <-> -. E. x e. A ps )
4	2 3	sylib	|- ( ph -> -. E. x e. A ps )