Theorem nrexdv 3273

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   ∈ wcel 2113  ∀wral 3141  ∃wrex 3142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1780  df-ral 3146  df-rex 3147

This theorem is referenced by:  class2set  5257  otiunsndisj  5413  peano5  7608  onnseq  7984  oalimcl  8189  omlimcl  8207  oeeulem  8230  nneob  8282  wemappo  9016  setind  9179  cardlim  9404  cardaleph  9518  cflim2  9688  fin23lem38  9774  isf32lem5  9782  winainflem  10118  winalim2  10121  supaddc  11611  supmul1  11613  ixxub  12762  ixxlb  12763  supicclub2  12892  s3iunsndisj  14331  rlimuni  14910  rlimcld2  14938  rlimno1  15013  harmonic  15217  eirr  15561  ruclem12  15597  dvdsle  15663  prmreclem5  16259  prmreclem6  16260  vdwnnlem3  16336  frgpnabllem1  18996  ablfacrplem  19190  lbsextlem3  19935  lmmo  21991  fbasfip  22479  hauspwpwf1  22598  alexsublem  22655  tsmsfbas  22739  iccntr  23432  reconnlem2  23438  evth  23566  bcthlem5  23934  minveclem3b  24034  itg2seq  24346  dvferm1  24585  dvferm2  24587  aaliou3lem9  24942  taylthlem2  24965  vma1  25746  pntlem3  26188  ostth2lem1  26197  tglowdim1i  26290  ssmxidllem  30982  ordtconnlem1  31171  ballotlemimin  31767  poseq  33099  frrlem14  33140  nosupbnd1lem4  33215  nocvxminlem  33251  tailfb  33729  unblimceq0  33850  fdc  35024  heibor1lem  35091  heiborlem8  35100  atlatmstc  36459  pmap0  36905  hdmap14lem4a  39011  cmpfiiin  39300  limcrecl  41916  dirkercncflem2  42396  fourierdlem20  42419  fourierdlem42  42441  fourierdlem46  42444  fourierdlem63  42461  fourierdlem64  42462  fourierdlem65  42463  otiunsndisjX  43485