Theorem nrexdv 3229

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107

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 1911

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-ral 3111  df-rex 3112

This theorem is referenced by:  class2set  5219  otiunsndisj  5375  peano5  7585  onnseq  7964  oalimcl  8169  omlimcl  8187  oeeulem  8210  nneob  8262  wemappo  8997  setind  9160  cardlim  9385  cardaleph  9500  cflim2  9674  fin23lem38  9760  isf32lem5  9768  winainflem  10104  winalim2  10107  supaddc  11595  supmul1  11597  ixxub  12747  ixxlb  12748  supicclub2  12882  s3iunsndisj  14319  rlimuni  14899  rlimcld2  14927  rlimno1  15002  harmonic  15206  eirr  15550  ruclem12  15586  dvdsle  15652  prmreclem5  16246  prmreclem6  16247  vdwnnlem3  16323  frgpnabllem1  18986  ablfacrplem  19180  lbsextlem3  19925  lmmo  21985  fbasfip  22473  hauspwpwf1  22592  alexsublem  22649  tsmsfbas  22733  iccntr  23426  reconnlem2  23432  evth  23564  bcthlem5  23932  minveclem3b  24032  itg2seq  24346  dvferm1  24588  dvferm2  24590  aaliou3lem9  24946  taylthlem2  24969  vma1  25751  pntlem3  26193  ostth2lem1  26202  tglowdim1i  26295  ssmxidllem  31049  ordtconnlem1  31277  ballotlemimin  31873  poseq  33208  frrlem14  33249  nosupbnd1lem4  33324  nocvxminlem  33360  tailfb  33838  unblimceq0  33959  fdc  35183  heibor1lem  35247  heiborlem8  35256  atlatmstc  36615  pmap0  37061  hdmap14lem4a  39167  cmpfiiin  39638  limcrecl  42271  dirkercncflem2  42746  fourierdlem20  42769  fourierdlem42  42791  fourierdlem46  42794  fourierdlem63  42811  fourierdlem64  42812  fourierdlem65  42813  otiunsndisjX  43835