Theorem nrexdv 3157

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∈ wcel 2144  ∀wral 3076  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-ral 3077  df-rex 3087

This theorem is used by:  class2set  5315  otiunsndisj  5492  peano5  7906  poseq  8178  frrlem14  8321  onnseq  8356  oalimcl  8572  omlimcl  8590  oeeulem  8614  nneob  8669  wemappo  9547  setind  9752  cardlim  10057  cardaleph  10172  cflim2  10345  fin23lem38  10431  isf32lem5  10439  winainflem  10782  winalim2  10785  supaddc  12288  supmul1  12290  ixxub  13501  ixxlb  13502  supicclub2  13639  s3iunsndisj  15127  rlimuni  15723  rlimcld2  15751  rlimno1  15827  harmonic  16034  eirr  16379  ruclem12  16415  dvdsle  16486  prmreclem5  17104  prmreclem6  17105  vdwnnlem3  17181  frgpnabllem1  20093  ablfacrplem  20287  lbsextlem3  21444  lmmo  23704  fbasfip  24193  hauspwpwf1  24312  alexsublem  24369  tsmsfbas  24453  iccntr  25147  reconnlem2  25153  evth  25286  bcthlem5  25655  minveclem3b  25755  itg2seq  26069  dvferm1  26311  dvferm2  26313  aaliou3lem9  26683  taylthlem2  26707  vma1  27499  pntlem3  27942  ostth2lem1  27951  nosupbnd1lem4  28074  noinfbnd1lem4  28089  nocvxminlem  28146  tglowdim1i  28970  ssmxidllem  34045  constrcon  34453  ordtconnlem1  34603  ballotlemimin  35185  setindregs  35855  tailfb  37258  unblimceq0  37466  fdc  38773  heibor1lem  38837  heiborlem8  38846  atlatmstc  40470  pmap0  40916  hdmap14lem4a  43022  cmpfiiin  43802  limcrecl  46735  dirkercncflem2  47208  fourierdlem20  47231  fourierdlem42  47253  fourierdlem46  47256  fourierdlem63  47273  fourierdlem64  47274  fourierdlem65  47275  otiunsndisjX  48443  upgrimpths  49101