Theorem nrexdv 3163

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2146  ∀wral 3082  ∃wrex 3092

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 3083  df-rex 3093

This theorem is used by:  class2set  5330  otiunsndisj  5508  peano5  7899  poseq  8163  frrlem14  8305  onnseq  8340  oalimcl  8554  omlimcl  8572  oeeulem  8596  nneob  8651  wemappo  9521  setind  9726  cardlim  9977  cardaleph  10092  cflim2  10265  fin23lem38  10351  isf32lem5  10359  winainflem  10696  winalim2  10699  supaddc  12200  supmul1  12202  ixxub  13411  ixxlb  13412  supicclub2  13549  s3iunsndisj  15031  rlimuni  15627  rlimcld2  15655  rlimno1  15731  harmonic  15939  eirr  16286  ruclem12  16322  dvdsle  16393  prmreclem5  17005  prmreclem6  17006  vdwnnlem3  17082  frgpnabllem1  19974  ablfacrplem  20168  lbsextlem3  21321  lmmo  23574  fbasfip  24062  hauspwpwf1  24181  alexsublem  24238  tsmsfbas  24322  iccntr  25016  reconnlem2  25022  evth  25155  bcthlem5  25524  minveclem3b  25624  itg2seq  25938  dvferm1  26181  dvferm2  26183  aaliou3lem9  26550  taylthlem2  26574  vma1  27367  pntlem3  27810  ostth2lem1  27819  nosupbnd1lem4  27912  noinfbnd1lem4  27927  nocvxminlem  27984  tglowdim1i  28807  ssmxidllem  33787  constrcon  34195  ordtconnlem1  34345  ballotlemimin  34928  setindregs  35567  tailfb  36929  unblimceq0  37137  fdc  38437  heibor1lem  38501  heiborlem8  38510  atlatmstc  40134  pmap0  40580  hdmap14lem4a  42686  cmpfiiin  43469  limcrecl  46386  dirkercncflem2  46859  fourierdlem20  46882  fourierdlem42  46904  fourierdlem46  46907  fourierdlem63  46924  fourierdlem64  46925  fourierdlem65  46926  otiunsndisjX  48057  upgrimpths  48715