Theorem nrex 3216

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 3100	. 2 ⊢ ∀𝑥 ∈ 𝐴 ¬ 𝜓
3		ralnex 3185	. 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓)
4	2, 3	mpbi 222	1 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2051  ∀wral 3090  ∃wrex 3091

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

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1744  df-ral 3095  df-rex 3096

This theorem is referenced by:  rex0  4206  iun0  4856  canth  6940  orduninsuc  7380  wfrlem16  7780  wofib  8810  cfsuc  9483  nominpos  11690  nnunb  11709  indstr  12136  eirr  15424  sqrt2irr  15468  vdwap0  16174  psgnunilem3  18398  bwth  21737  zfbas  22223  aaliou3lem9  24657  vma1  25460  hatomistici  29935  esumrnmpt2  31003  linedegen  33165  limsucncmpi  33353  elpadd0  36430  fourierdlem62  41919  etransc  42034  0nodd  43480  2nodd  43482  1neven  43602