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

Theorem nrexdv 3147
Description: Deduction adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) (Proof shortened by Wolf Lammen, 5-Jan-2020.)
Hypothesis
Ref Expression
nrexdv.1 ((𝜑𝑥𝐴) → ¬ 𝜓)
Assertion
Ref Expression
nrexdv (𝜑 → ¬ ∃𝑥𝐴 𝜓)
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem nrexdv
StepHypRef Expression
1 nrexdv.1 . . 3 ((𝜑𝑥𝐴) → ¬ 𝜓)
21ralrimiva 3113 . 2 (𝜑 → ∀𝑥𝐴 ¬ 𝜓)
3 ralnex 3139 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3sylib 209 1 (𝜑 → ¬ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wcel 2155  wral 3055  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-ral 3060  df-rex 3061
This theorem is referenced by:  class2set  4992  otiunsndisj  5143  peano5  7289  onnseq  7647  oalimcl  7847  omlimcl  7865  oeeulem  7888  nneob  7939  wemappo  8663  setind  8827  cardlim  9051  cardaleph  9165  cflim2  9340  fin23lem38  9426  isf32lem5  9434  winainflem  9770  winalim2  9773  supaddc  11246  supmul1  11248  ixxub  12401  ixxlb  12402  supicclub2  12533  s3iunsndisj  13997  rlimuni  14569  rlimcld2  14597  rlimno1  14672  harmonic  14878  eirr  15218  ruclem12  15255  dvdsle  15320  prmreclem5  15906  prmreclem6  15907  vdwnnlem3  15983  frgpnabllem1  18545  ablfacrplem  18734  lbsextlem3  19437  lmmo  21467  fbasfip  21954  hauspwpwf1  22073  alexsublem  22130  tsmsfbas  22213  iccntr  22906  reconnlem2  22912  evth  23040  bcthlem5  23408  minveclem3b  23491  itg2seq  23803  dvferm1  24042  dvferm2  24044  aaliou3lem9  24399  taylthlem2  24422  vma1  25186  pntlem3  25592  ostth2lem1  25601  tglowdim1i  25690  ordtconnlem1  30420  ballotlemimin  31018  poseq  32200  nosupbnd1lem4  32304  nocvxminlem  32340  tailfb  32818  fdc  33966  heibor1lem  34033  heiborlem8  34042  atlatmstc  35278  pmap0  35724  hdmap14lem4a  37830  cmpfiiin  37941  limcrecl  40502  dirkercncflem2  40961  fourierdlem20  40984  fourierdlem42  41006  fourierdlem46  41009  fourierdlem63  41026  fourierdlem64  41027  fourierdlem65  41028  otiunsndisjX  42031
  Copyright terms: Public domain W3C validator