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  5302  otiunsndisj  5476  peano5  7845  poseq  8110  frrlem14  8251  onnseq  8286  oalimcl  8497  omlimcl  8515  oeeulem  8539  nneob  8594  wemappo  9466  setind  9668  cardlim  9896  cardaleph  10011  cflim2  10185  fin23lem38  10271  isf32lem5  10279  winainflem  10616  winalim2  10619  supaddc  12121  supmul1  12123  ixxub  13294  ixxlb  13295  supicclub2  13432  s3iunsndisj  14903  rlimuni  15485  rlimcld2  15513  rlimno1  15589  harmonic  15794  eirr  16142  ruclem12  16178  dvdsle  16249  prmreclem5  16860  prmreclem6  16861  vdwnnlem3  16937  frgpnabllem1  19814  ablfacrplem  20008  lbsextlem3  21127  lmmo  23336  fbasfip  23824  hauspwpwf1  23943  alexsublem  24000  tsmsfbas  24084  iccntr  24778  reconnlem2  24784  evth  24926  bcthlem5  25296  minveclem3b  25396  itg2seq  25711  dvferm1  25957  dvferm2  25959  aaliou3lem9  26326  taylthlem2  26350  taylthlem2OLD  26351  vma1  27144  pntlem3  27588  ostth2lem1  27597  nosupbnd1lem4  27691  noinfbnd1lem4  27706  nocvxminlem  27762  tglowdim1i  28585  ssmxidllem  33565  constrcon  33951  ordtconnlem1  34101  ballotlemimin  34683  setindregs  35305  tailfb  36590  unblimceq0  36726  fdc  37993  heibor1lem  38057  heiborlem8  38066  atlatmstc  39692  pmap0  40138  hdmap14lem4a  42244  cmpfiiin  43051  limcrecl  45986  dirkercncflem2  46459  fourierdlem20  46482  fourierdlem42  46504  fourierdlem46  46507  fourierdlem63  46524  fourierdlem64  46525  fourierdlem65  46526  otiunsndisjX  47636  upgrimpths  48266