Theorem nrexdv 3148

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2107  ∀wral 3060  ∃wrex 3069

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-ral 3061  df-rex 3070

This theorem is referenced by:  class2set  5354  otiunsndisj  5524  peano5  7916  poseq  8184  frrlem14  8325  onnseq  8385  oalimcl  8599  omlimcl  8617  oeeulem  8640  nneob  8695  wemappo  9590  setind  9775  cardlim  10013  cardaleph  10130  cflim2  10304  fin23lem38  10390  isf32lem5  10398  winainflem  10734  winalim2  10737  supaddc  12236  supmul1  12238  ixxub  13409  ixxlb  13410  supicclub2  13545  s3iunsndisj  15008  rlimuni  15587  rlimcld2  15615  rlimno1  15691  harmonic  15896  eirr  16242  ruclem12  16278  dvdsle  16348  prmreclem5  16959  prmreclem6  16960  vdwnnlem3  17036  frgpnabllem1  19892  ablfacrplem  20086  lbsextlem3  21163  lmmo  23389  fbasfip  23877  hauspwpwf1  23996  alexsublem  24053  tsmsfbas  24137  iccntr  24844  reconnlem2  24850  evth  24992  bcthlem5  25363  minveclem3b  25463  itg2seq  25778  dvferm1  26024  dvferm2  26026  aaliou3lem9  26393  taylthlem2  26417  taylthlem2OLD  26418  vma1  27210  pntlem3  27654  ostth2lem1  27663  nosupbnd1lem4  27757  noinfbnd1lem4  27772  nocvxminlem  27823  tglowdim1i  28510  ssmxidllem  33502  ordtconnlem1  33924  ballotlemimin  34509  tailfb  36379  unblimceq0  36509  fdc  37753  heibor1lem  37817  heiborlem8  37826  atlatmstc  39321  pmap0  39768  hdmap14lem4a  41874  cmpfiiin  42713  limcrecl  45649  dirkercncflem2  46124  fourierdlem20  46147  fourierdlem42  46169  fourierdlem46  46172  fourierdlem63  46189  fourierdlem64  46190  fourierdlem65  46191  otiunsndisjX  47296