Theorem nrexdv 3160

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2145  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-ral 3080  df-rex 3090

This theorem is referenced by:  class2set  5315  otiunsndisj  5493  peano5  7878  poseq  8142  frrlem14  8284  onnseq  8319  oalimcl  8533  omlimcl  8551  oeeulem  8575  nneob  8630  wemappo  9499  setind  9704  cardlim  9946  cardaleph  10061  cflim2  10235  fin23lem38  10321  isf32lem5  10329  winainflem  10666  winalim2  10669  supaddc  12170  supmul1  12172  ixxub  13381  ixxlb  13382  supicclub2  13519  s3iunsndisj  14993  rlimuni  15589  rlimcld2  15617  rlimno1  15693  harmonic  15901  eirr  16249  ruclem12  16285  dvdsle  16356  prmreclem5  16968  prmreclem6  16969  vdwnnlem3  17045  frgpnabllem1  19931  ablfacrplem  20125  lbsextlem3  21250  lmmo  23494  fbasfip  23982  hauspwpwf1  24101  alexsublem  24158  tsmsfbas  24242  iccntr  24936  reconnlem2  24942  evth  25075  bcthlem5  25444  minveclem3b  25544  itg2seq  25858  dvferm1  26101  dvferm2  26103  aaliou3lem9  26468  taylthlem2  26491  vma1  27284  pntlem3  27727  ostth2lem1  27736  nosupbnd1lem4  27829  noinfbnd1lem4  27844  nocvxminlem  27901  tglowdim1i  28724  ssmxidllem  33668  constrcon  34076  ordtconnlem1  34226  ballotlemimin  34808  setindregs  35433  tailfb  36745  unblimceq0  36953  fdc  38251  heibor1lem  38315  heiborlem8  38324  atlatmstc  39950  pmap0  40396  hdmap14lem4a  42502  cmpfiiin  43285  limcrecl  46204  dirkercncflem2  46677  fourierdlem20  46700  fourierdlem42  46722  fourierdlem46  46725  fourierdlem63  46742  fourierdlem64  46743  fourierdlem65  46744  otiunsndisjX  47872  upgrimpths  48530