Theorem nrexdv 3127

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056

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 3048  df-rex 3057

This theorem is referenced by:  class2set  5293  otiunsndisj  5460  peano5  7823  poseq  8088  frrlem14  8229  onnseq  8264  oalimcl  8475  omlimcl  8493  oeeulem  8516  nneob  8571  wemappo  9435  setind  9637  cardlim  9865  cardaleph  9980  cflim2  10154  fin23lem38  10240  isf32lem5  10248  winainflem  10584  winalim2  10587  supaddc  12089  supmul1  12091  ixxub  13266  ixxlb  13267  supicclub2  13404  s3iunsndisj  14875  rlimuni  15457  rlimcld2  15485  rlimno1  15561  harmonic  15766  eirr  16114  ruclem12  16150  dvdsle  16221  prmreclem5  16832  prmreclem6  16833  vdwnnlem3  16909  frgpnabllem1  19786  ablfacrplem  19980  lbsextlem3  21098  lmmo  23296  fbasfip  23784  hauspwpwf1  23903  alexsublem  23960  tsmsfbas  24044  iccntr  24738  reconnlem2  24744  evth  24886  bcthlem5  25256  minveclem3b  25356  itg2seq  25671  dvferm1  25917  dvferm2  25919  aaliou3lem9  26286  taylthlem2  26310  taylthlem2OLD  26311  vma1  27104  pntlem3  27548  ostth2lem1  27557  nosupbnd1lem4  27651  noinfbnd1lem4  27666  nocvxminlem  27718  tglowdim1i  28480  ssmxidllem  33436  constrcon  33785  ordtconnlem1  33935  ballotlemimin  34517  setindregs  35126  tailfb  36417  unblimceq0  36547  fdc  37791  heibor1lem  37855  heiborlem8  37864  atlatmstc  39364  pmap0  39810  hdmap14lem4a  41916  cmpfiiin  42736  limcrecl  45675  dirkercncflem2  46148  fourierdlem20  46171  fourierdlem42  46193  fourierdlem46  46196  fourierdlem63  46213  fourierdlem64  46214  fourierdlem65  46215  otiunsndisjX  47316  upgrimpths  47946