Theorem nrexdv 3128

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

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

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 3049  df-rex 3058

This theorem is referenced by:  class2set  5297  otiunsndisj  5465  peano5  7831  poseq  8096  frrlem14  8237  onnseq  8272  oalimcl  8483  omlimcl  8501  oeeulem  8524  nneob  8579  wemappo  9444  setind  9646  cardlim  9874  cardaleph  9989  cflim2  10163  fin23lem38  10249  isf32lem5  10257  winainflem  10593  winalim2  10596  supaddc  12098  supmul1  12100  ixxub  13270  ixxlb  13271  supicclub2  13408  s3iunsndisj  14879  rlimuni  15461  rlimcld2  15489  rlimno1  15565  harmonic  15770  eirr  16118  ruclem12  16154  dvdsle  16225  prmreclem5  16836  prmreclem6  16837  vdwnnlem3  16913  frgpnabllem1  19789  ablfacrplem  19983  lbsextlem3  21101  lmmo  23298  fbasfip  23786  hauspwpwf1  23905  alexsublem  23962  tsmsfbas  24046  iccntr  24740  reconnlem2  24746  evth  24888  bcthlem5  25258  minveclem3b  25358  itg2seq  25673  dvferm1  25919  dvferm2  25921  aaliou3lem9  26288  taylthlem2  26312  taylthlem2OLD  26313  vma1  27106  pntlem3  27550  ostth2lem1  27559  nosupbnd1lem4  27653  noinfbnd1lem4  27668  nocvxminlem  27720  tglowdim1i  28482  ssmxidllem  33447  constrcon  33810  ordtconnlem1  33960  ballotlemimin  34542  setindregs  35151  tailfb  36444  unblimceq0  36574  fdc  37808  heibor1lem  37872  heiborlem8  37881  atlatmstc  39441  pmap0  39887  hdmap14lem4a  41993  cmpfiiin  42817  limcrecl  45756  dirkercncflem2  46229  fourierdlem20  46252  fourierdlem42  46274  fourierdlem46  46277  fourierdlem63  46294  fourierdlem64  46295  fourierdlem65  46296  otiunsndisjX  47406  upgrimpths  48036