Theorem nrex 2192

Description: Inference adding restricted existential quantifier to negated wff.

Hypothesis

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

Assertion

Ref	Expression
nrex	|- -. E.x e. A ps

Proof of Theorem nrex

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

Syntax hints:  -. wn 2   -> wi 3   e. wcel 1300  A.wral 2105  E.wrex 2106

This theorem is referenced by:  rex0 2888  iun0 3309  iun0OLD 3310  orduninsuc 3925  0nelqs 5357  cfsuc 6063  nominpos 7230  nnunb 7279  indstr 7630  sqr2irrlem3 7976  climubii 8413  eirr 8656  ruclem37 8815  hatomistici 11934  wfrlem16 13972  heiborlem14 15968  elpadd0 17270

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-4 1319  ax-5o 1321

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-ral 2109  df-rex 2110

Copyright terms: Public domain