Theorem nrexdv 3133

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

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

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 3053  df-rex 3063

This theorem is referenced by:  class2set  5292  otiunsndisj  5468  peano5  7837  poseq  8101  frrlem14  8242  onnseq  8277  oalimcl  8488  omlimcl  8506  oeeulem  8530  nneob  8585  wemappo  9457  setind  9659  cardlim  9887  cardaleph  10002  cflim2  10176  fin23lem38  10262  isf32lem5  10270  winainflem  10607  winalim2  10610  supaddc  12114  supmul1  12116  ixxub  13310  ixxlb  13311  supicclub2  13448  s3iunsndisj  14921  rlimuni  15503  rlimcld2  15531  rlimno1  15607  harmonic  15815  eirr  16163  ruclem12  16199  dvdsle  16270  prmreclem5  16882  prmreclem6  16883  vdwnnlem3  16959  frgpnabllem1  19839  ablfacrplem  20033  lbsextlem3  21150  lmmo  23355  fbasfip  23843  hauspwpwf1  23962  alexsublem  24019  tsmsfbas  24103  iccntr  24797  reconnlem2  24803  evth  24936  bcthlem5  25305  minveclem3b  25405  itg2seq  25719  dvferm1  25962  dvferm2  25964  aaliou3lem9  26327  taylthlem2  26351  taylthlem2OLD  26352  vma1  27143  pntlem3  27586  ostth2lem1  27595  nosupbnd1lem4  27689  noinfbnd1lem4  27704  nocvxminlem  27760  tglowdim1i  28583  ssmxidllem  33548  constrcon  33934  ordtconnlem1  34084  ballotlemimin  34666  setindregs  35290  tailfb  36575  unblimceq0  36783  fdc  38080  heibor1lem  38144  heiborlem8  38153  atlatmstc  39779  pmap0  40225  hdmap14lem4a  42331  cmpfiiin  43143  limcrecl  46077  dirkercncflem2  46550  fourierdlem20  46573  fourierdlem42  46595  fourierdlem46  46598  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  otiunsndisjX  47739  upgrimpths  48397