Theorem nrexdv 3159

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

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

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 3079  df-rex 3089

This theorem is used by:  class2set  5323  otiunsndisj  5501  peano5  7894  poseq  8160  frrlem14  8302  onnseq  8337  oalimcl  8551  omlimcl  8569  oeeulem  8593  nneob  8648  wemappo  9525  setind  9730  cardlim  9981  cardaleph  10096  cflim2  10269  fin23lem38  10355  isf32lem5  10363  winainflem  10706  winalim2  10709  supaddc  12210  supmul1  12212  ixxub  13423  ixxlb  13424  supicclub2  13561  s3iunsndisj  15045  rlimuni  15641  rlimcld2  15669  rlimno1  15745  harmonic  15952  eirr  16299  ruclem12  16335  dvdsle  16406  prmreclem5  17018  prmreclem6  17019  vdwnnlem3  17095  frgpnabllem1  20006  ablfacrplem  20200  lbsextlem3  21353  lmmo  23611  fbasfip  24100  hauspwpwf1  24219  alexsublem  24276  tsmsfbas  24360  iccntr  25054  reconnlem2  25060  evth  25193  bcthlem5  25562  minveclem3b  25662  itg2seq  25976  dvferm1  26219  dvferm2  26221  aaliou3lem9  26593  taylthlem2  26617  vma1  27410  pntlem3  27853  ostth2lem1  27862  nosupbnd1lem4  27955  noinfbnd1lem4  27970  nocvxminlem  28027  tglowdim1i  28851  ssmxidllem  33884  constrcon  34292  ordtconnlem1  34442  ballotlemimin  35025  setindregs  35664  tailfb  37004  unblimceq0  37212  fdc  38503  heibor1lem  38567  heiborlem8  38576  atlatmstc  40200  pmap0  40646  hdmap14lem4a  42752  cmpfiiin  43550  limcrecl  46467  dirkercncflem2  46940  fourierdlem20  46963  fourierdlem42  46985  fourierdlem46  46988  fourierdlem63  47005  fourierdlem64  47006  fourierdlem65  47007  otiunsndisjX  48175  upgrimpths  48833