Theorem nrexdv 3135

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∈ wcel 2119  ∀wral 3054  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-ral 3055  df-rex 3065

This theorem is referenced by:  class2set  5290  otiunsndisj  5468  peano5  7840  poseq  8105  frrlem14  8246  onnseq  8281  oalimcl  8492  omlimcl  8510  oeeulem  8534  nneob  8589  wemappo  9461  setind  9666  cardlim  9894  cardaleph  10009  cflim2  10183  fin23lem38  10269  isf32lem5  10277  winainflem  10614  winalim2  10617  supaddc  12121  supmul1  12123  ixxub  13317  ixxlb  13318  supicclub2  13455  s3iunsndisj  14928  rlimuni  15510  rlimcld2  15538  rlimno1  15614  harmonic  15822  eirr  16170  ruclem12  16206  dvdsle  16277  prmreclem5  16889  prmreclem6  16890  vdwnnlem3  16966  frgpnabllem1  19846  ablfacrplem  20040  lbsextlem3  21160  lmmo  23370  fbasfip  23858  hauspwpwf1  23977  alexsublem  24034  tsmsfbas  24118  iccntr  24812  reconnlem2  24818  evth  24951  bcthlem5  25320  minveclem3b  25420  itg2seq  25734  dvferm1  25977  dvferm2  25979  aaliou3lem9  26341  taylthlem2  26364  vma1  27154  pntlem3  27597  ostth2lem1  27606  nosupbnd1lem4  27700  noinfbnd1lem4  27715  nocvxminlem  27771  tglowdim1i  28594  ssmxidllem  33563  constrcon  33965  ordtconnlem1  34115  ballotlemimin  34697  setindregs  35318  tailfb  36612  unblimceq0  36820  fdc  38119  heibor1lem  38183  heiborlem8  38192  atlatmstc  39818  pmap0  40264  hdmap14lem4a  42370  cmpfiiin  43153  limcrecl  46081  dirkercncflem2  46554  fourierdlem20  46577  fourierdlem42  46599  fourierdlem46  46602  fourierdlem63  46619  fourierdlem64  46620  fourierdlem65  46621  otiunsndisjX  47749  upgrimpths  48407