Theorem nrexdv 3150

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2107  ∀wral 3062  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-ral 3063  df-rex 3072

This theorem is referenced by:  class2set  5354  otiunsndisj  5521  peano5  7884  peano5OLD  7885  poseq  8144  frrlem14  8284  onnseq  8344  oalimcl  8560  omlimcl  8578  oeeulem  8601  nneob  8655  wemappo  9544  setind  9729  cardlim  9967  cardaleph  10084  cflim2  10258  fin23lem38  10344  isf32lem5  10352  winainflem  10688  winalim2  10691  supaddc  12181  supmul1  12183  ixxub  13345  ixxlb  13346  supicclub2  13481  s3iunsndisj  14915  rlimuni  15494  rlimcld2  15522  rlimno1  15600  harmonic  15805  eirr  16148  ruclem12  16184  dvdsle  16253  prmreclem5  16853  prmreclem6  16854  vdwnnlem3  16930  frgpnabllem1  19741  ablfacrplem  19935  lbsextlem3  20773  lmmo  22884  fbasfip  23372  hauspwpwf1  23491  alexsublem  23548  tsmsfbas  23632  iccntr  24337  reconnlem2  24343  evth  24475  bcthlem5  24845  minveclem3b  24945  itg2seq  25260  dvferm1  25502  dvferm2  25504  aaliou3lem9  25863  taylthlem2  25886  vma1  26670  pntlem3  27112  ostth2lem1  27121  nosupbnd1lem4  27214  noinfbnd1lem4  27229  nocvxminlem  27279  tglowdim1i  27783  ssmxidllem  32620  ordtconnlem1  32935  ballotlemimin  33535  tailfb  35310  unblimceq0  35431  fdc  36661  heibor1lem  36725  heiborlem8  36734  atlatmstc  38237  pmap0  38684  hdmap14lem4a  40790  cmpfiiin  41483  limcrecl  44393  dirkercncflem2  44868  fourierdlem20  44891  fourierdlem42  44913  fourierdlem46  44916  fourierdlem63  44933  fourierdlem64  44934  fourierdlem65  44935  otiunsndisjX  46035