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

Theorem nrexdv 2997
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 2962 . 2 (𝜑 → ∀𝑥𝐴 ¬ 𝜓)
3 ralnex 2988 . 2 (∀𝑥𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥𝐴 𝜓)
42, 3sylib 208 1 (𝜑 → ¬ ∃𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 384  wcel 1987  wral 2908  wrex 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-ral 2913  df-rex 2914
This theorem is referenced by:  class2set  4802  otiunsndisj  4950  peano5  7051  onnseq  7401  oalimcl  7600  omlimcl  7618  oeeulem  7641  nneob  7692  wemappo  8414  setind  8570  cardlim  8758  cardaleph  8872  cflim2  9045  fin23lem38  9131  isf32lem5  9139  winainflem  9475  winalim2  9478  supaddc  10950  supmul1  10952  ixxub  12154  ixxlb  12155  supicclub2  12281  s3iunsndisj  13657  rlimuni  14231  rlimcld2  14259  rlimno1  14334  harmonic  14535  eirr  14877  ruclem12  14914  dvdsle  14975  prmreclem5  15567  prmreclem6  15568  vdwnnlem3  15644  frgpnabllem1  18216  ablfacrplem  18404  lbsextlem3  19100  lmmo  21124  fbasfip  21612  hauspwpwf1  21731  alexsublem  21788  tsmsfbas  21871  iccntr  22564  reconnlem2  22570  evth  22698  bcthlem5  23065  minveclem3b  23139  itg2seq  23449  dvferm1  23686  dvferm2  23688  aaliou3lem9  24043  taylthlem2  24066  vma1  24826  pntlem3  25232  ostth2lem1  25241  tglowdim1i  25330  ordtconnlem1  29794  ballotlemimin  30390  poseq  31504  nocvxminlem  31606  tailfb  32067  fdc  33212  heibor1lem  33279  heiborlem8  33288  atlatmstc  34125  pmap0  34570  hdmap14lem4a  36682  cmpfiiin  36779  limcrecl  39297  dirkercncflem2  39658  fourierdlem20  39681  fourierdlem42  39703  fourierdlem46  39706  fourierdlem63  39723  fourierdlem64  39724  fourierdlem65  39725  otiunsndisjX  40625
  Copyright terms: Public domain W3C validator