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

Theorem nrex 3147
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 3070 . 2 𝑥𝐴 ¬ 𝜓
3 ralnex 3140 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3mpbi 220 1 ¬ ∃𝑥𝐴 𝜓
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wcel 2144  wral 3060  wrex 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1852  df-ral 3065  df-rex 3066
This theorem is referenced by:  rex0  4083  iun0  4708  canth  6750  orduninsuc  7189  wfrlem16  7582  wofib  8605  cfsuc  9280  nominpos  11470  nnunb  11489  indstr  11958  eirr  15138  sqrt2irr  15184  vdwap0  15886  psgnunilem3  18122  bwth  21433  zfbas  21919  aaliou3lem9  24324  vma1  25112  hatomistici  29555  esumrnmpt2  30464  linedegen  32581  limsucncmpi  32775  elpadd0  35610  fourierdlem62  40896  etransc  41011  0nodd  42328  2nodd  42330  1neven  42450
  Copyright terms: Public domain W3C validator