HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem nrexdv 1722
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
StepHypRef Expression
1 nrexdv.1 . . 3 |- ((ph /\ x e. A) -> -. ps)
21r19.21aiva 1706 . 2 |- (ph -> A.x e. A -. ps)
3 ralnex 1645 . 2 |- (A.x e. A -. ps <-> -. E.x e. A ps)
42, 3sylib 198 1 |- (ph -> -. E.x e. A ps)
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   /\ wa 223   e. wcel 955  A.wral 1637  E.wrex 1638
This theorem is referenced by:  class2set 2724  peano5 3143  oalimcl 4178  omlimcl 4193  nneob 4239  setind 4620  cardlim 4823  cardaleph 4857  dffsum 6936  climrecl 7047  climge0 7049  caucvglem6 7098  dfisum 7127  eirr 7335
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-17 968  ax-4 970  ax-5o 972
This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-ral 1641  df-rex 1642
Copyright terms: Public domain