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

Theorem nrexdv 3262
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 3176 . 2 (𝜑 → ∀𝑥𝐴 ¬ 𝜓)
3 ralnex 3230 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3sylib 221 1 (𝜑 → ¬ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399  wcel 2115  wral 3132  wrex 3133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3137  df-rex 3138
This theorem is referenced by:  class2set  5235  otiunsndisj  5391  peano5  7588  onnseq  7964  oalimcl  8169  omlimcl  8187  oeeulem  8210  nneob  8262  wemappo  8997  setind  9160  cardlim  9385  cardaleph  9500  cflim2  9670  fin23lem38  9756  isf32lem5  9764  winainflem  10100  winalim2  10103  supaddc  11593  supmul1  11595  ixxub  12745  ixxlb  12746  supicclub2  12880  s3iunsndisj  14317  rlimuni  14896  rlimcld2  14924  rlimno1  14999  harmonic  15203  eirr  15547  ruclem12  15583  dvdsle  15649  prmreclem5  16243  prmreclem6  16244  vdwnnlem3  16320  frgpnabllem1  18982  ablfacrplem  19176  lbsextlem3  19918  lmmo  21974  fbasfip  22462  hauspwpwf1  22581  alexsublem  22638  tsmsfbas  22722  iccntr  23415  reconnlem2  23421  evth  23553  bcthlem5  23921  minveclem3b  24021  itg2seq  24335  dvferm1  24577  dvferm2  24579  aaliou3lem9  24935  taylthlem2  24958  vma1  25740  pntlem3  26182  ostth2lem1  26191  tglowdim1i  26284  ssmxidllem  30999  ordtconnlem1  31185  ballotlemimin  31781  poseq  33113  frrlem14  33154  nosupbnd1lem4  33229  nocvxminlem  33265  tailfb  33743  unblimceq0  33864  fdc  35083  heibor1lem  35147  heiborlem8  35156  atlatmstc  36515  pmap0  36961  hdmap14lem4a  39067  cmpfiiin  39470  limcrecl  42113  dirkercncflem2  42588  fourierdlem20  42611  fourierdlem42  42633  fourierdlem46  42636  fourierdlem63  42653  fourierdlem64  42654  fourierdlem65  42655  otiunsndisjX  43677
  Copyright terms: Public domain W3C validator