Theorem nrex

Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003)

	Ref	Expression
Hypothesis	nrex.1	|- ( x e. A -> -. ps )
Assertion	nrex	|- -. E. x e. A ps

Proof

Step	Hyp	Ref	Expression
1		nrex.1	|- ( x e. A -> -. ps )
2	1	rgen	|- A. x e. A -. ps
3		ralnex	|- ( A. x e. A -. ps <-> -. E. x e. A ps )
4	2 3	mpbi	|- -. E. x e. A ps