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

Theorem nrex 3187
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 3110 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 3180 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 221 1 ¬ ∃𝑥𝐴 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2156  wral 3096  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-ral 3101  df-rex 3102
This theorem is referenced by:  rex0  4139  iun0  4768  canth  6832  orduninsuc  7273  wfrlem16  7666  wofib  8689  cfsuc  9364  nominpos  11536  nnunb  11555  indstr  11975  eirr  15153  sqrt2irr  15199  vdwap0  15897  psgnunilem3  18117  bwth  21427  zfbas  21913  aaliou3lem9  24319  vma1  25106  hatomistici  29549  esumrnmpt2  30455  linedegen  32571  limsucncmpi  32761  elpadd0  35589  fourierdlem62  40864  etransc  40979  0nodd  42378  2nodd  42380  1neven  42500
  Copyright terms: Public domain W3C validator