Theorem nrexdv 3132

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2114  ∀wral 3051  ∃wrex 3061

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 207  df-an 396  df-ex 1782  df-ral 3052  df-rex 3062

This theorem is referenced by:  class2set  5296  otiunsndisj  5474  peano5  7844  poseq  8108  frrlem14  8249  onnseq  8284  oalimcl  8495  omlimcl  8513  oeeulem  8537  nneob  8592  wemappo  9464  setind  9668  cardlim  9896  cardaleph  10011  cflim2  10185  fin23lem38  10271  isf32lem5  10279  winainflem  10616  winalim2  10619  supaddc  12123  supmul1  12125  ixxub  13319  ixxlb  13320  supicclub2  13457  s3iunsndisj  14930  rlimuni  15512  rlimcld2  15540  rlimno1  15616  harmonic  15824  eirr  16172  ruclem12  16208  dvdsle  16279  prmreclem5  16891  prmreclem6  16892  vdwnnlem3  16968  frgpnabllem1  19848  ablfacrplem  20042  lbsextlem3  21158  lmmo  23345  fbasfip  23833  hauspwpwf1  23952  alexsublem  24009  tsmsfbas  24093  iccntr  24787  reconnlem2  24793  evth  24926  bcthlem5  25295  minveclem3b  25395  itg2seq  25709  dvferm1  25952  dvferm2  25954  aaliou3lem9  26316  taylthlem2  26339  vma1  27129  pntlem3  27572  ostth2lem1  27581  nosupbnd1lem4  27675  noinfbnd1lem4  27690  nocvxminlem  27746  tglowdim1i  28569  ssmxidllem  33533  constrcon  33918  ordtconnlem1  34068  ballotlemimin  34650  setindregs  35274  tailfb  36559  unblimceq0  36767  fdc  38066  heibor1lem  38130  heiborlem8  38139  atlatmstc  39765  pmap0  40211  hdmap14lem4a  42317  cmpfiiin  43129  limcrecl  46059  dirkercncflem2  46532  fourierdlem20  46555  fourierdlem42  46577  fourierdlem46  46580  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  otiunsndisjX  47727  upgrimpths  48385