Theorem nrexdv 3160

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  class2set  5327  otiunsndisj  5505  peano5  7891  poseq  8155  frrlem14  8297  onnseq  8332  oalimcl  8546  omlimcl  8564  oeeulem  8588  nneob  8643  wemappo  9512  setind  9717  cardlim  9959  cardaleph  10074  cflim2  10248  fin23lem38  10334  isf32lem5  10342  winainflem  10679  winalim2  10682  supaddc  12183  supmul1  12185  ixxub  13394  ixxlb  13395  supicclub2  13532  s3iunsndisj  15007  rlimuni  15603  rlimcld2  15631  rlimno1  15707  harmonic  15915  eirr  16262  ruclem12  16298  dvdsle  16369  prmreclem5  16981  prmreclem6  16982  vdwnnlem3  17058  frgpnabllem1  19944  ablfacrplem  20138  lbsextlem3  21265  lmmo  23518  fbasfip  24006  hauspwpwf1  24125  alexsublem  24182  tsmsfbas  24266  iccntr  24960  reconnlem2  24966  evth  25099  bcthlem5  25468  minveclem3b  25568  itg2seq  25882  dvferm1  26125  dvferm2  26127  aaliou3lem9  26494  taylthlem2  26518  vma1  27311  pntlem3  27754  ostth2lem1  27763  nosupbnd1lem4  27856  noinfbnd1lem4  27871  nocvxminlem  27928  tglowdim1i  28751  ssmxidllem  33737  constrcon  34145  ordtconnlem1  34295  ballotlemimin  34877  setindregs  35524  tailfb  36869  unblimceq0  37077  fdc  38377  heibor1lem  38441  heiborlem8  38450  atlatmstc  40074  pmap0  40520  hdmap14lem4a  42626  cmpfiiin  43411  limcrecl  46328  dirkercncflem2  46801  fourierdlem20  46824  fourierdlem42  46846  fourierdlem46  46849  fourierdlem63  46866  fourierdlem64  46867  fourierdlem65  46868  otiunsndisjX  47999  upgrimpths  48657