Theorem nrexdv 3124

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 3121	. 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  5297  otiunsndisj  5467  peano5  7833  poseq  8098  frrlem14  8239  onnseq  8274  oalimcl  8485  omlimcl  8503  oeeulem  8526  nneob  8581  wemappo  9460  setind  9649  cardlim  9887  cardaleph  10002  cflim2  10176  fin23lem38  10262  isf32lem5  10270  winainflem  10606  winalim2  10609  supaddc  12110  supmul1  12112  ixxub  13287  ixxlb  13288  supicclub2  13425  s3iunsndisj  14893  rlimuni  15475  rlimcld2  15503  rlimno1  15579  harmonic  15784  eirr  16132  ruclem12  16168  dvdsle  16239  prmreclem5  16850  prmreclem6  16851  vdwnnlem3  16927  frgpnabllem1  19770  ablfacrplem  19964  lbsextlem3  21085  lmmo  23283  fbasfip  23771  hauspwpwf1  23890  alexsublem  23947  tsmsfbas  24031  iccntr  24726  reconnlem2  24732  evth  24874  bcthlem5  25244  minveclem3b  25344  itg2seq  25659  dvferm1  25905  dvferm2  25907  aaliou3lem9  26274  taylthlem2  26298  taylthlem2OLD  26299  vma1  27092  pntlem3  27536  ostth2lem1  27545  nosupbnd1lem4  27639  noinfbnd1lem4  27654  nocvxminlem  27706  tglowdim1i  28464  ssmxidllem  33423  constrcon  33743  ordtconnlem1  33893  ballotlemimin  34476  setindregs  35067  tailfb  36353  unblimceq0  36483  fdc  37727  heibor1lem  37791  heiborlem8  37800  atlatmstc  39300  pmap0  39747  hdmap14lem4a  41853  cmpfiiin  42673  limcrecl  45614  dirkercncflem2  46089  fourierdlem20  46112  fourierdlem42  46134  fourierdlem46  46137  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  otiunsndisjX  47267  upgrimpths  47897