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

Theorem nrex 3074
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 3063 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 3072 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 230 1 ¬ ∃𝑥𝐴 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2108  wral 3061  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3062  df-rex 3071
This theorem is referenced by:  rex0  4360  iun0  5062  canth  7385  orduninsuc  7864  wfrlem16OLD  8364  wofib  9585  cfsuc  10297  nominpos  12503  nnunb  12522  indstr  12958  eirr  16241  sqrt2irr  16285  vdwap0  17014  smndex1n0mnd  18925  smndex2dnrinv  18928  psgnunilem3  19514  bwth  23418  zfbas  23904  aaliou3lem9  26392  vma1  27209  muls01  28138  mulsrid  28139  onmulscl  28287  hatomistici  32381  esumrnmpt2  34069  fmlan0  35396  linedegen  36144  limsucncmpi  36446  elpadd0  39811  rexanuz2nf  45503  fourierdlem62  46183  etransc  46298  0nodd  48086  2nodd  48088  1neven  48154
  Copyright terms: Public domain W3C validator