Theorem nrexdv 1776

Description: Deduction adding restricted existential quantifier to negated wff.

Hypothesis

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

Assertion

Ref	Expression
nrexdv	|- (ph -> -. E.x e. A ps)

Distinct variable group:   ph,x

Proof of Theorem nrexdv

Step	Hyp	Ref	Expression
1		nrexdv.1	. . 3 |- ((ph /\ x e. A) -> -. ps)
2	1	r19.21aiva 1760	. 2 |- (ph -> A.x e. A -. ps)
3		ralnex 1699	. 2 |- (A.x e. A -. ps <-> -. E.x e. A ps)
4	2, 3	sylib 196	1 |- (ph -> -. E.x e. A ps)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 221   e. wcel 994  A.wral 1691  E.wrex 1692

This theorem is referenced by:  class2set 2808  peano5 3241  oalimcl 4330  omlimcl 4345  nneob 4395  ac6sfilem3 4590  setind 4794  cardlim 5001  cardaleph 5035  dffsum 7201  climrecl 7313  climge0 7315  caucvglem6 7365  dfisum 7395  eirr 7599  fgfil 11638  tailfb 11762

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-17 1007  ax-4 1009  ax-5o 1011

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-ral 1695  df-rex 1696

Copyright terms: Public domain