Theorem nrexdv 3141

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2098  ∀wral 3053  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1774  df-ral 3054  df-rex 3063

This theorem is referenced by:  class2set  5343  otiunsndisj  5510  peano5  7877  peano5OLD  7878  poseq  8138  frrlem14  8279  onnseq  8339  oalimcl  8555  omlimcl  8573  oeeulem  8596  nneob  8651  wemappo  9540  setind  9725  cardlim  9963  cardaleph  10080  cflim2  10254  fin23lem38  10340  isf32lem5  10348  winainflem  10684  winalim2  10687  supaddc  12178  supmul1  12180  ixxub  13342  ixxlb  13343  supicclub2  13478  s3iunsndisj  14912  rlimuni  15491  rlimcld2  15519  rlimno1  15597  harmonic  15802  eirr  16145  ruclem12  16181  dvdsle  16250  prmreclem5  16852  prmreclem6  16853  vdwnnlem3  16929  frgpnabllem1  19783  ablfacrplem  19977  lbsextlem3  21001  lmmo  23206  fbasfip  23694  hauspwpwf1  23813  alexsublem  23870  tsmsfbas  23954  iccntr  24659  reconnlem2  24665  evth  24807  bcthlem5  25178  minveclem3b  25278  itg2seq  25594  dvferm1  25839  dvferm2  25841  aaliou3lem9  26204  taylthlem2  26227  vma1  27014  pntlem3  27458  ostth2lem1  27467  nosupbnd1lem4  27560  noinfbnd1lem4  27575  nocvxminlem  27626  tglowdim1i  28221  ssmxidllem  33058  ordtconnlem1  33393  ballotlemimin  33993  gg-taylthlem2  35657  tailfb  35752  unblimceq0  35873  fdc  37103  heibor1lem  37167  heiborlem8  37176  atlatmstc  38679  pmap0  39126  hdmap14lem4a  41232  cmpfiiin  41924  limcrecl  44830  dirkercncflem2  45305  fourierdlem20  45328  fourierdlem42  45350  fourierdlem46  45353  fourierdlem63  45370  fourierdlem64  45371  fourierdlem65  45372  otiunsndisjX  46472