Theorem nrexdv 3156

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   ∈ wcel 2141  ∀wral 3075  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-ral 3076  df-rex 3086

This theorem is referenced by:  class2set  5308  otiunsndisj  5486  peano5  7868  poseq  8131  frrlem14  8273  onnseq  8308  oalimcl  8522  omlimcl  8540  oeeulem  8564  nneob  8619  wemappo  9490  setind  9695  cardlim  9923  cardaleph  10038  cflim2  10213  fin23lem38  10299  isf32lem5  10307  winainflem  10644  winalim2  10647  supaddc  12152  supmul1  12154  ixxub  13363  ixxlb  13364  supicclub2  13501  s3iunsndisj  14974  rlimuni  15567  rlimcld2  15595  rlimno1  15671  harmonic  15879  eirr  16227  ruclem12  16263  dvdsle  16334  prmreclem5  16946  prmreclem6  16947  vdwnnlem3  17023  frgpnabllem1  19903  ablfacrplem  20097  lbsextlem3  21217  lmmo  23427  fbasfip  23915  hauspwpwf1  24034  alexsublem  24091  tsmsfbas  24175  iccntr  24869  reconnlem2  24875  evth  25008  bcthlem5  25377  minveclem3b  25477  itg2seq  25791  dvferm1  26034  dvferm2  26036  aaliou3lem9  26401  taylthlem2  26424  vma1  27217  pntlem3  27660  ostth2lem1  27669  nosupbnd1lem4  27762  noinfbnd1lem4  27777  nocvxminlem  27834  tglowdim1i  28657  ssmxidllem  33621  constrcon  34031  ordtconnlem1  34181  ballotlemimin  34763  setindregs  35386  tailfb  36697  unblimceq0  36905  fdc  38204  heibor1lem  38268  heiborlem8  38277  atlatmstc  39903  pmap0  40349  hdmap14lem4a  42455  cmpfiiin  43238  limcrecl  46165  dirkercncflem2  46638  fourierdlem20  46661  fourierdlem42  46683  fourierdlem46  46686  fourierdlem63  46703  fourierdlem64  46704  fourierdlem65  46705  otiunsndisjX  47833  upgrimpths  48491