MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nrex Unicode version

Theorem nrex 2912
Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)
Hypothesis
Ref Expression
nrex.1
Assertion
Ref Expression
nrex

Proof of Theorem nrex
StepHypRef Expression
1 nrex.1 . . 3
21rgen 2817 . 2
3 ralnex 2903 . 2
42, 3mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  e.wcel 1818  A.wral 2807  E.wrex 2808
This theorem is referenced by:  rex0  3799  iun0  4386  canth  6254  orduninsuc  6678  wofib  7991  cfsuc  8658  nominpos  10800  nnunb  10816  indstr  11179  eirr  13938  sqrt2irr  13982  vdwap0  14494  psgnunilem3  16521  bwth  19910  zfbas  20397  aaliou3lem9  22746  vma1  23440  hatomistici  27281  wfrlem16  29358  linedegen  29793  limsucncmpi  29910  fourierdlem62  31951  etransc  32066  0nodd  32498  2nodd  32500  1neven  32738  elpadd0  35533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-ral 2812  df-rex 2813
  Copyright terms: Public domain W3C validator