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

Theorem nrex 3029
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 2951 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 3021 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 220 1 ¬ ∃𝑥𝐴 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2030  wral 2941  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  rex0  3971  iun0  4608  canth  6648  orduninsuc  7085  wfrlem16  7475  wofib  8491  cfsuc  9117  nominpos  11307  nnunb  11326  indstr  11794  eirr  14977  sqrt2irr  15023  vdwap0  15727  psgnunilem3  17962  bwth  21261  zfbas  21747  aaliou3lem9  24150  vma1  24937  hatomistici  29349  esumrnmpt2  30258  linedegen  32375  limsucncmpi  32569  elpadd0  35413  fourierdlem62  40703  etransc  40818  0nodd  42135  2nodd  42137  1neven  42257
  Copyright terms: Public domain W3C validator