Theorem nrexdv 3155

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 3152	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ¬ 𝜓)
3		ralnex 3078	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
4	2, 3	sylib 218	1 ⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐴 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2108  ∀wral 3067  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-ral 3068  df-rex 3077

This theorem is referenced by:  class2set  5373  otiunsndisj  5539  peano5  7932  peano5OLD  7933  poseq  8199  frrlem14  8340  onnseq  8400  oalimcl  8616  omlimcl  8634  oeeulem  8657  nneob  8712  wemappo  9618  setind  9803  cardlim  10041  cardaleph  10158  cflim2  10332  fin23lem38  10418  isf32lem5  10426  winainflem  10762  winalim2  10765  supaddc  12262  supmul1  12264  ixxub  13428  ixxlb  13429  supicclub2  13564  s3iunsndisj  15017  rlimuni  15596  rlimcld2  15624  rlimno1  15702  harmonic  15907  eirr  16253  ruclem12  16289  dvdsle  16358  prmreclem5  16967  prmreclem6  16968  vdwnnlem3  17044  frgpnabllem1  19915  ablfacrplem  20109  lbsextlem3  21185  lmmo  23409  fbasfip  23897  hauspwpwf1  24016  alexsublem  24073  tsmsfbas  24157  iccntr  24862  reconnlem2  24868  evth  25010  bcthlem5  25381  minveclem3b  25481  itg2seq  25797  dvferm1  26043  dvferm2  26045  aaliou3lem9  26410  taylthlem2  26434  taylthlem2OLD  26435  vma1  27227  pntlem3  27671  ostth2lem1  27680  nosupbnd1lem4  27774  noinfbnd1lem4  27789  nocvxminlem  27840  tglowdim1i  28527  ssmxidllem  33466  ordtconnlem1  33870  ballotlemimin  34470  tailfb  36343  unblimceq0  36473  fdc  37705  heibor1lem  37769  heiborlem8  37778  atlatmstc  39275  pmap0  39722  hdmap14lem4a  41828  cmpfiiin  42653  limcrecl  45550  dirkercncflem2  46025  fourierdlem20  46048  fourierdlem42  46070  fourierdlem46  46073  fourierdlem63  46090  fourierdlem64  46091  fourierdlem65  46092  otiunsndisjX  47194