Theorem nrexdv 3143

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 397   ∈ wcel 2104  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1780  df-ral 3063  df-rex 3072

This theorem is referenced by:  class2set  5285  otiunsndisj  5447  peano5  7772  peano5OLD  7773  frrlem14  8146  onnseq  8206  oalimcl  8422  omlimcl  8440  oeeulem  8463  nneob  8517  wemappo  9352  setind  9536  cardlim  9774  cardaleph  9891  cflim2  10065  fin23lem38  10151  isf32lem5  10159  winainflem  10495  winalim2  10498  supaddc  11988  supmul1  11990  ixxub  13146  ixxlb  13147  supicclub2  13282  s3iunsndisj  14724  rlimuni  15304  rlimcld2  15332  rlimno1  15410  harmonic  15616  eirr  15959  ruclem12  15995  dvdsle  16064  prmreclem5  16666  prmreclem6  16667  vdwnnlem3  16743  frgpnabllem1  19519  ablfacrplem  19713  lbsextlem3  20467  lmmo  22576  fbasfip  23064  hauspwpwf1  23183  alexsublem  23240  tsmsfbas  23324  iccntr  24029  reconnlem2  24035  evth  24167  bcthlem5  24537  minveclem3b  24637  itg2seq  24952  dvferm1  25194  dvferm2  25196  aaliou3lem9  25555  taylthlem2  25578  vma1  26360  pntlem3  26802  ostth2lem1  26811  tglowdim1i  26907  ssmxidllem  31686  ordtconnlem1  31919  ballotlemimin  32517  poseq  33847  nosupbnd1lem4  33959  noinfbnd1lem4  33974  nocvxminlem  34017  tailfb  34611  unblimceq0  34732  fdc  35947  heibor1lem  36011  heiborlem8  36020  atlatmstc  37375  pmap0  37821  hdmap14lem4a  39927  cmpfiiin  40556  limcrecl  43219  dirkercncflem2  43694  fourierdlem20  43717  fourierdlem42  43739  fourierdlem46  43742  fourierdlem63  43759  fourierdlem64  43760  fourierdlem65  43761  otiunsndisjX  44829