Theorem nrexdv 1730

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 1714	. 2 |- (ph -> A.x e. A -. ps)
3		ralnex 1653	. 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 958  A.wral 1645  E.wrex 1646

This theorem is referenced by:  class2set 2734  peano5 3153  oalimcl 4194  omlimcl 4209  nneob 4255  setind 4648  cardlim 4851  cardaleph 4885  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 963  ax-17 971  ax-4 973  ax-5o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-ral 1649  df-rex 1650

Copyright terms: Public domain