Theorem nrex 3075

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2106  ∀wral 3062  ∃wrex 3071

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

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1782  df-ral 3063  df-rex 3072

This theorem is referenced by:  rex0  4308  iun0  5013  canth  7294  orduninsuc  7761  wfrlem16OLD  8229  wofib  9406  cfsuc  10118  nominpos  12315  nnunb  12334  indstr  12761  eirr  16013  sqrt2irr  16057  vdwap0  16774  smndex1n0mnd  18647  smndex2dnrinv  18650  psgnunilem3  19200  bwth  22666  zfbas  23152  aaliou3lem9  25615  vma1  26420  hatomistici  31011  esumrnmpt2  32332  fmlan0  33650  linedegen  34582  limsucncmpi  34771  elpadd0  38128  fourierdlem62  44097  etransc  44212  0nodd  45782  2nodd  45784  1neven  45908