Theorem nrexdv 3131

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-ral 3052  df-rex 3061

This theorem is referenced by:  class2set  5300  otiunsndisj  5468  peano5  7835  poseq  8100  frrlem14  8241  onnseq  8276  oalimcl  8487  omlimcl  8505  oeeulem  8529  nneob  8584  wemappo  9454  setind  9656  cardlim  9884  cardaleph  9999  cflim2  10173  fin23lem38  10259  isf32lem5  10267  winainflem  10604  winalim2  10607  supaddc  12109  supmul1  12111  ixxub  13282  ixxlb  13283  supicclub2  13420  s3iunsndisj  14891  rlimuni  15473  rlimcld2  15501  rlimno1  15577  harmonic  15782  eirr  16130  ruclem12  16166  dvdsle  16237  prmreclem5  16848  prmreclem6  16849  vdwnnlem3  16925  frgpnabllem1  19802  ablfacrplem  19996  lbsextlem3  21115  lmmo  23324  fbasfip  23812  hauspwpwf1  23931  alexsublem  23988  tsmsfbas  24072  iccntr  24766  reconnlem2  24772  evth  24914  bcthlem5  25284  minveclem3b  25384  itg2seq  25699  dvferm1  25945  dvferm2  25947  aaliou3lem9  26314  taylthlem2  26338  taylthlem2OLD  26339  vma1  27132  pntlem3  27576  ostth2lem1  27585  nosupbnd1lem4  27679  noinfbnd1lem4  27694  nocvxminlem  27750  tglowdim1i  28573  ssmxidllem  33554  constrcon  33931  ordtconnlem1  34081  ballotlemimin  34663  setindregs  35286  tailfb  36571  unblimceq0  36707  fdc  37946  heibor1lem  38010  heiborlem8  38019  atlatmstc  39579  pmap0  40025  hdmap14lem4a  42131  cmpfiiin  42939  limcrecl  45875  dirkercncflem2  46348  fourierdlem20  46371  fourierdlem42  46393  fourierdlem46  46396  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  otiunsndisjX  47525  upgrimpths  48155