Theorem nrexdv 3161

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

Step	Hyp	Ref	Expression
1		nrexdv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ¬ 𝜓)
2	1	ralrimiva 3158	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝜓)
3		ralnex 3092	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
4	2, 3	sylib 221	1 ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  class2set  5321  otiunsndisj  5498  peano5  7932  poseq  8205  frrlem14  8348  onnseq  8383  oalimcl  8599  omlimcl  8617  oeeulem  8641  nneob  8696  wemappo  9573  setind  9778  cardlim  10083  cardaleph  10198  cflim2  10371  fin23lem38  10457  isf32lem5  10465  winainflem  10808  winalim2  10811  supaddc  12314  supmul1  12316  ixxub  13527  ixxlb  13528  supicclub2  13665  s3iunsndisj  15153  rlimuni  15749  rlimcld2  15777  rlimno1  15853  harmonic  16060  eirr  16405  ruclem12  16441  dvdsle  16512  prmreclem5  17130  prmreclem6  17131  vdwnnlem3  17207  frgpnabllem1  20120  ablfacrplem  20314  lbsextlem3  21471  lmmo  23731  fbasfip  24220  hauspwpwf1  24339  alexsublem  24396  tsmsfbas  24480  iccntr  25174  reconnlem2  25180  evth  25313  bcthlem5  25682  minveclem3b  25782  itg2seq  26096  dvferm1  26338  dvferm2  26340  aaliou3lem9  26710  taylthlem2  26734  vma1  27526  pntlem3  27969  ostth2lem1  27978  nosupbnd1lem4  28101  noinfbnd1lem4  28116  nocvxminlem  28173  tglowdim1i  28997  ssmxidllem  34082  constrcon  34489  ordtconnlem1  34639  ballotlemimin  35221  setindregs  35911  tailfb  37356  unblimceq0  37564  fdc  38882  heibor1lem  38946  heiborlem8  38955  atlatmstc  40579  pmap0  41025  hdmap14lem4a  43131  cmpfiiin  43912  limcrecl  46856  dirkercncflem2  47329  fourierdlem20  47352  fourierdlem42  47374  fourierdlem46  47377  fourierdlem63  47394  fourierdlem64  47395  fourierdlem65  47396  otiunsndisjX  48564  upgrimpths  49222