Theorem nrexdv 3209

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 386   ∈ wcel 2164  ∀wral 3117  ∃wrex 3118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1879  df-ral 3122  df-rex 3123

This theorem is referenced by:  class2set  5056  otiunsndisj  5208  peano5  7355  onnseq  7712  oalimcl  7912  omlimcl  7930  oeeulem  7953  nneob  8004  wemappo  8730  setind  8894  cardlim  9118  cardaleph  9232  cflim2  9407  fin23lem38  9493  isf32lem5  9501  winainflem  9837  winalim2  9840  supaddc  11327  supmul1  11329  ixxub  12491  ixxlb  12492  supicclub2  12623  s3iunsndisj  14093  rlimuni  14665  rlimcld2  14693  rlimno1  14768  harmonic  14972  eirr  15314  ruclem12  15351  dvdsle  15416  prmreclem5  16002  prmreclem6  16003  vdwnnlem3  16079  frgpnabllem1  18636  ablfacrplem  18825  lbsextlem3  19528  lmmo  21562  fbasfip  22049  hauspwpwf1  22168  alexsublem  22225  tsmsfbas  22308  iccntr  23001  reconnlem2  23007  evth  23135  bcthlem5  23503  minveclem3b  23603  itg2seq  23915  dvferm1  24154  dvferm2  24156  aaliou3lem9  24511  taylthlem2  24534  vma1  25312  pntlem3  25718  ostth2lem1  25727  tglowdim1i  25820  ordtconnlem1  30511  ballotlemimin  31109  poseq  32287  nosupbnd1lem4  32391  nocvxminlem  32427  tailfb  32905  fdc  34082  heibor1lem  34149  heiborlem8  34158  atlatmstc  35393  pmap0  35839  hdmap14lem4a  37945  cmpfiiin  38103  limcrecl  40654  dirkercncflem2  41113  fourierdlem20  41136  fourierdlem42  41158  fourierdlem46  41161  fourierdlem63  41178  fourierdlem64  41179  fourierdlem65  41180  otiunsndisjX  42180