Theorem nrexdv 3136

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3053  df-rex 3062

This theorem is referenced by:  class2set  5330  otiunsndisj  5500  peano5  7894  poseq  8162  frrlem14  8303  onnseq  8363  oalimcl  8577  omlimcl  8595  oeeulem  8618  nneob  8673  wemappo  9568  setind  9753  cardlim  9991  cardaleph  10108  cflim2  10282  fin23lem38  10368  isf32lem5  10376  winainflem  10712  winalim2  10715  supaddc  12214  supmul1  12216  ixxub  13388  ixxlb  13389  supicclub2  13526  s3iunsndisj  14992  rlimuni  15571  rlimcld2  15599  rlimno1  15675  harmonic  15880  eirr  16228  ruclem12  16264  dvdsle  16334  prmreclem5  16945  prmreclem6  16946  vdwnnlem3  17022  frgpnabllem1  19859  ablfacrplem  20053  lbsextlem3  21126  lmmo  23323  fbasfip  23811  hauspwpwf1  23930  alexsublem  23987  tsmsfbas  24071  iccntr  24766  reconnlem2  24772  evth  24914  bcthlem5  25285  minveclem3b  25385  itg2seq  25700  dvferm1  25946  dvferm2  25948  aaliou3lem9  26315  taylthlem2  26339  taylthlem2OLD  26340  vma1  27133  pntlem3  27577  ostth2lem1  27586  nosupbnd1lem4  27680  noinfbnd1lem4  27695  nocvxminlem  27746  tglowdim1i  28485  ssmxidllem  33493  constrcon  33813  ordtconnlem1  33960  ballotlemimin  34543  tailfb  36400  unblimceq0  36530  fdc  37774  heibor1lem  37838  heiborlem8  37847  atlatmstc  39342  pmap0  39789  hdmap14lem4a  41895  cmpfiiin  42695  limcrecl  45638  dirkercncflem2  46113  fourierdlem20  46136  fourierdlem42  46158  fourierdlem46  46161  fourierdlem63  46178  fourierdlem64  46179  fourierdlem65  46180  otiunsndisjX  47288  upgrimpths  47902