Theorem nrexdv 3270

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2110  ∀wral 3138  ∃wrex 3139

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-ral 3143  df-rex 3144

This theorem is referenced by:  class2set  5247  otiunsndisj  5403  peano5  7599  onnseq  7975  oalimcl  8180  omlimcl  8198  oeeulem  8221  nneob  8273  wemappo  9007  setind  9170  cardlim  9395  cardaleph  9509  cflim2  9679  fin23lem38  9765  isf32lem5  9773  winainflem  10109  winalim2  10112  supaddc  11602  supmul1  11604  ixxub  12753  ixxlb  12754  supicclub2  12883  s3iunsndisj  14322  rlimuni  14901  rlimcld2  14929  rlimno1  15004  harmonic  15208  eirr  15552  ruclem12  15588  dvdsle  15654  prmreclem5  16250  prmreclem6  16251  vdwnnlem3  16327  frgpnabllem1  18987  ablfacrplem  19181  lbsextlem3  19926  lmmo  21982  fbasfip  22470  hauspwpwf1  22589  alexsublem  22646  tsmsfbas  22730  iccntr  23423  reconnlem2  23429  evth  23557  bcthlem5  23925  minveclem3b  24025  itg2seq  24337  dvferm1  24576  dvferm2  24578  aaliou3lem9  24933  taylthlem2  24956  vma1  25737  pntlem3  26179  ostth2lem1  26188  tglowdim1i  26281  ssmxidllem  30973  ordtconnlem1  31162  ballotlemimin  31758  poseq  33090  frrlem14  33131  nosupbnd1lem4  33206  nocvxminlem  33242  tailfb  33720  unblimceq0  33841  fdc  35014  heibor1lem  35081  heiborlem8  35090  atlatmstc  36449  pmap0  36895  hdmap14lem4a  39001  cmpfiiin  39287  limcrecl  41902  dirkercncflem2  42382  fourierdlem20  42405  fourierdlem42  42427  fourierdlem46  42430  fourierdlem63  42447  fourierdlem64  42448  fourierdlem65  42449  otiunsndisjX  43471