Theorem nrexdv 2984

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∈ wcel 1977  ∀wral 2896  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  class2set  4758  otiunsndisj  4905  peano5  6981  onnseq  7328  oalimcl  7527  omlimcl  7545  oeeulem  7568  nneob  7619  wemappo  8337  setind  8493  cardlim  8681  cardaleph  8795  cflim2  8968  fin23lem38  9054  isf32lem5  9062  winainflem  9394  winalim2  9397  supaddc  10867  supmul1  10869  ixxub  12067  ixxlb  12068  supicclub2  12194  s3iunsndisj  13555  rlimuni  14129  rlimcld2  14157  rlimno1  14232  harmonic  14430  eirr  14772  ruclem12  14809  dvdsle  14870  prmreclem5  15462  prmreclem6  15463  vdwnnlem3  15539  frgpnabllem1  18099  ablfacrplem  18287  lbsextlem3  18981  lmmo  20994  fbasfip  21482  hauspwpwf1  21601  alexsublem  21658  tsmsfbas  21741  iccntr  22432  reconnlem2  22438  evth  22566  bcthlem5  22933  minveclem3b  23007  itg2seq  23315  dvferm1  23552  dvferm2  23554  aaliou3lem9  23909  taylthlem2  23932  vma1  24692  pntlem3  25098  ostth2lem1  25107  tglowdim1i  25196  2spotiundisj  26589  2spot0  26591  ordtconlem1  29298  ballotlemimin  29894  poseq  30994  nocvxminlem  31089  tailfb  31542  fdc  32711  heibor1lem  32778  heiborlem8  32787  atlatmstc  33624  pmap0  34069  hdmap14lem4a  36181  cmpfiiin  36278  limcrecl  38696  dirkercncflem2  38997  fourierdlem20  39020  fourierdlem42  39042  fourierdlem46  39045  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  otiunsndisjX  40317