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

Theorem nrexdv 3139
 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 3104 . 2 (𝜑 → ∀𝑥𝐴 ¬ 𝜓)
3 ralnex 3130 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3sylib 208 1 (𝜑 → ¬ ∃𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∈ wcel 2139  ∀wral 3050  ∃wrex 3051 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056 This theorem is referenced by:  class2set  4981  otiunsndisj  5130  peano5  7254  onnseq  7610  oalimcl  7809  omlimcl  7827  oeeulem  7850  nneob  7901  wemappo  8619  setind  8783  cardlim  8988  cardaleph  9102  cflim2  9277  fin23lem38  9363  isf32lem5  9371  winainflem  9707  winalim2  9710  supaddc  11182  supmul1  11184  ixxub  12389  ixxlb  12390  supicclub2  12516  s3iunsndisj  13908  rlimuni  14480  rlimcld2  14508  rlimno1  14583  harmonic  14790  eirr  15132  ruclem12  15169  dvdsle  15234  prmreclem5  15826  prmreclem6  15827  vdwnnlem3  15903  frgpnabllem1  18476  ablfacrplem  18664  lbsextlem3  19362  lmmo  21386  fbasfip  21873  hauspwpwf1  21992  alexsublem  22049  tsmsfbas  22132  iccntr  22825  reconnlem2  22831  evth  22959  bcthlem5  23325  minveclem3b  23399  itg2seq  23708  dvferm1  23947  dvferm2  23949  aaliou3lem9  24304  taylthlem2  24327  vma1  25091  pntlem3  25497  ostth2lem1  25506  tglowdim1i  25595  ordtconnlem1  30279  ballotlemimin  30876  poseq  32059  nosupbnd1lem4  32163  nocvxminlem  32199  tailfb  32678  fdc  33854  heibor1lem  33921  heiborlem8  33930  atlatmstc  35109  pmap0  35554  hdmap14lem4a  37665  cmpfiiin  37762  limcrecl  40364  dirkercncflem2  40824  fourierdlem20  40847  fourierdlem42  40869  fourierdlem46  40872  fourierdlem63  40889  fourierdlem64  40890  fourierdlem65  40891  otiunsndisjX  41806
 Copyright terms: Public domain W3C validator