Theorem nrexdv 3147

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2106  ∀wral 3059  ∃wrex 3068

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-ral 3060  df-rex 3069

This theorem is referenced by:  class2set  5361  otiunsndisj  5530  peano5  7916  poseq  8182  frrlem14  8323  onnseq  8383  oalimcl  8597  omlimcl  8615  oeeulem  8638  nneob  8693  wemappo  9587  setind  9772  cardlim  10010  cardaleph  10127  cflim2  10301  fin23lem38  10387  isf32lem5  10395  winainflem  10731  winalim2  10734  supaddc  12233  supmul1  12235  ixxub  13405  ixxlb  13406  supicclub2  13541  s3iunsndisj  15004  rlimuni  15583  rlimcld2  15611  rlimno1  15687  harmonic  15892  eirr  16238  ruclem12  16274  dvdsle  16344  prmreclem5  16954  prmreclem6  16955  vdwnnlem3  17031  frgpnabllem1  19906  ablfacrplem  20100  lbsextlem3  21180  lmmo  23404  fbasfip  23892  hauspwpwf1  24011  alexsublem  24068  tsmsfbas  24152  iccntr  24857  reconnlem2  24863  evth  25005  bcthlem5  25376  minveclem3b  25476  itg2seq  25792  dvferm1  26038  dvferm2  26040  aaliou3lem9  26407  taylthlem2  26431  taylthlem2OLD  26432  vma1  27224  pntlem3  27668  ostth2lem1  27677  nosupbnd1lem4  27771  noinfbnd1lem4  27786  nocvxminlem  27837  tglowdim1i  28524  ssmxidllem  33481  ordtconnlem1  33885  ballotlemimin  34487  tailfb  36360  unblimceq0  36490  fdc  37732  heibor1lem  37796  heiborlem8  37805  atlatmstc  39301  pmap0  39748  hdmap14lem4a  41854  cmpfiiin  42685  limcrecl  45585  dirkercncflem2  46060  fourierdlem20  46083  fourierdlem42  46105  fourierdlem46  46108  fourierdlem63  46125  fourierdlem64  46126  fourierdlem65  46127  otiunsndisjX  47229