Theorem nrexdv 3199

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3065  ∃wrex 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1786  df-ral 3070  df-rex 3071

This theorem is referenced by:  class2set  5279  otiunsndisj  5436  peano5  7727  peano5OLD  7728  frrlem14  8099  onnseq  8159  oalimcl  8367  omlimcl  8385  oeeulem  8408  nneob  8460  wemappo  9269  setind  9475  cardlim  9714  cardaleph  9829  cflim2  10003  fin23lem38  10089  isf32lem5  10097  winainflem  10433  winalim2  10436  supaddc  11925  supmul1  11927  ixxub  13082  ixxlb  13083  supicclub2  13218  s3iunsndisj  14660  rlimuni  15240  rlimcld2  15268  rlimno1  15346  harmonic  15552  eirr  15895  ruclem12  15931  dvdsle  16000  prmreclem5  16602  prmreclem6  16603  vdwnnlem3  16679  frgpnabllem1  19455  ablfacrplem  19649  lbsextlem3  20403  lmmo  22512  fbasfip  23000  hauspwpwf1  23119  alexsublem  23176  tsmsfbas  23260  iccntr  23965  reconnlem2  23971  evth  24103  bcthlem5  24473  minveclem3b  24573  itg2seq  24888  dvferm1  25130  dvferm2  25132  aaliou3lem9  25491  taylthlem2  25514  vma1  26296  pntlem3  26738  ostth2lem1  26747  tglowdim1i  26843  ssmxidllem  31620  ordtconnlem1  31853  ballotlemimin  32451  poseq  33781  nosupbnd1lem4  33893  noinfbnd1lem4  33908  nocvxminlem  33951  tailfb  34545  unblimceq0  34666  fdc  35882  heibor1lem  35946  heiborlem8  35955  atlatmstc  37312  pmap0  37758  hdmap14lem4a  39864  cmpfiiin  40499  limcrecl  43124  dirkercncflem2  43599  fourierdlem20  43622  fourierdlem42  43644  fourierdlem46  43647  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  otiunsndisjX  44722