Theorem nrexdv 3158

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2145  ∀wral 3077  ∃wrex 3087

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3078  df-rex 3088

This theorem is used by:  class2set  5316  otiunsndisj  5493  peano5  7894  poseq  8159  frrlem14  8301  onnseq  8336  oalimcl  8552  omlimcl  8570  oeeulem  8594  nneob  8649  wemappo  9527  setind  9732  cardlim  10034  cardaleph  10149  cflim2  10322  fin23lem38  10408  isf32lem5  10416  winainflem  10759  winalim2  10762  supaddc  12265  supmul1  12267  ixxub  13478  ixxlb  13479  supicclub2  13616  s3iunsndisj  15101  rlimuni  15697  rlimcld2  15725  rlimno1  15801  harmonic  16008  eirr  16353  ruclem12  16389  dvdsle  16460  prmreclem5  17078  prmreclem6  17079  vdwnnlem3  17155  frgpnabllem1  20067  ablfacrplem  20261  lbsextlem3  21418  lmmo  23678  fbasfip  24167  hauspwpwf1  24286  alexsublem  24343  tsmsfbas  24427  iccntr  25121  reconnlem2  25127  evth  25260  bcthlem5  25629  minveclem3b  25729  itg2seq  26043  dvferm1  26285  dvferm2  26287  aaliou3lem9  26659  taylthlem2  26683  vma1  27475  pntlem3  27918  ostth2lem1  27927  nosupbnd1lem4  28050  noinfbnd1lem4  28065  nocvxminlem  28122  tglowdim1i  28946  ssmxidllem  33980  constrcon  34388  ordtconnlem1  34538  ballotlemimin  35121  setindregs  35771  tailfb  37135  unblimceq0  37343  fdc  38647  heibor1lem  38711  heiborlem8  38720  atlatmstc  40344  pmap0  40790  hdmap14lem4a  42896  cmpfiiin  43661  limcrecl  46585  dirkercncflem2  47058  fourierdlem20  47081  fourierdlem42  47103  fourierdlem46  47106  fourierdlem63  47123  fourierdlem64  47124  fourierdlem65  47125  otiunsndisjX  48293  upgrimpths  48951