Theorem nrexdv 1733

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 1717	. 2 |- (ph -> A.x e. A -. ps)
3		ralnex 1656	. 2 |- (A.x e. A -. ps <-> -. E.x e. A ps)
4	2, 3	sylib 198	1 |- (ph -> -. E.x e. A ps)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   e. wcel 960  A.wral 1648  E.wrex 1649

This theorem is referenced by:  class2set 2739  peano5 3159  oalimcl 4200  omlimcl 4215  nneob 4261  setind 4658  cardlim 4862  cardaleph 4896  dffsum 6998  climrecl 7110  climge0 7112  caucvglem6 7162  dfisum 7191  eirr 7394

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-ral 1652  df-rex 1653

Copyright terms: Public domain