Theorem nrex 3100

Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.)

Hypothesis

Ref	Expression
nrex.1	⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓)

Assertion

Ref	Expression
nrex	⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓

Proof of Theorem nrex

Step	Hyp	Ref	Expression
1		nrex.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓)
2	1	rgen 3088	. 2 ⊢ ∀𝑥 ∈ 𝐴 ¬ 𝜓
3		ralnex 3098	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbi 233	1 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2150  ∀wral 3086  ∃wrex 3096

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-ral 3087  df-rex 3097

This theorem is referenced by:  rex0  4323  iun0  5031  canth  7368  orduninsuc  7842  wofib  9510  cfsuc  10244  nominpos  12484  nnunb  12503  indstr  12943  eirr  16264  sqrt2irr  16308  vdwap0  17039  smndex1n0mnd  18977  smndex2dnrinv  18980  psgnunilem3  19569  bwth  23550  zfbas  24036  aaliou3lem9  26494  vma1  27310  muls01  28285  mulsrid  28286  onmulscl  28451  hatomistici  32684  esumrnmpt2  34428  fmlan0  35841  linedegen  36593  limsucncmpi  36904  ttcwf2  36984  mh-inf3sn  37001  elpadd0  40533  rexanuz2nf  46158  fourierdlem62  46834  etransc  46949  cjnpoly  47575  0nodd  48884  2nodd  48886  1neven  48952