Theorem nrexdv 3128

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

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

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 207  df-an 396  df-ex 1780  df-ral 3045  df-rex 3054

This theorem is referenced by:  class2set  5310  otiunsndisj  5480  peano5  7869  poseq  8137  frrlem14  8278  onnseq  8313  oalimcl  8524  omlimcl  8542  oeeulem  8565  nneob  8620  wemappo  9502  setind  9687  cardlim  9925  cardaleph  10042  cflim2  10216  fin23lem38  10302  isf32lem5  10310  winainflem  10646  winalim2  10649  supaddc  12150  supmul1  12152  ixxub  13327  ixxlb  13328  supicclub2  13465  s3iunsndisj  14934  rlimuni  15516  rlimcld2  15544  rlimno1  15620  harmonic  15825  eirr  16173  ruclem12  16209  dvdsle  16280  prmreclem5  16891  prmreclem6  16892  vdwnnlem3  16968  frgpnabllem1  19803  ablfacrplem  19997  lbsextlem3  21070  lmmo  23267  fbasfip  23755  hauspwpwf1  23874  alexsublem  23931  tsmsfbas  24015  iccntr  24710  reconnlem2  24716  evth  24858  bcthlem5  25228  minveclem3b  25328  itg2seq  25643  dvferm1  25889  dvferm2  25891  aaliou3lem9  26258  taylthlem2  26282  taylthlem2OLD  26283  vma1  27076  pntlem3  27520  ostth2lem1  27529  nosupbnd1lem4  27623  noinfbnd1lem4  27638  nocvxminlem  27689  tglowdim1i  28428  ssmxidllem  33444  constrcon  33764  ordtconnlem1  33914  ballotlemimin  34497  tailfb  36365  unblimceq0  36495  fdc  37739  heibor1lem  37803  heiborlem8  37812  atlatmstc  39312  pmap0  39759  hdmap14lem4a  41865  cmpfiiin  42685  limcrecl  45627  dirkercncflem2  46102  fourierdlem20  46125  fourierdlem42  46147  fourierdlem46  46150  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  otiunsndisjX  47280  upgrimpths  47909