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

Theorem nrex 2979
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 2902 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 2971 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 218 1 ¬ ∃𝑥𝐴 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 1976  wral 2892  wrex 2893
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2897  df-rex 2898
This theorem is referenced by:  rex0  3890  iun0  4503  canth  6483  orduninsuc  6909  wfrlem16  7291  wofib  8307  cfsuc  8936  nominpos  11113  nnunb  11132  indstr  11585  eirr  14715  sqrt2irr  14760  vdwap0  15461  psgnunilem3  17682  bwth  20962  zfbas  21449  aaliou3lem9  23823  vma1  24606  hatomistici  28408  esumrnmpt2  29260  linedegen  31223  limsucncmpi  31417  elpadd0  33913  fourierdlem62  38862  etransc  38977  0nodd  41599  2nodd  41601  1neven  41721
  Copyright terms: Public domain W3C validator