Theorem nrex 3178

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2112  ∀wral 3051  ∃wrex 3052

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3056  df-rex 3057

This theorem is referenced by:  rex0  4258  iun0  4956  canth  7145  orduninsuc  7600  wfrlem16  8048  wofib  9139  cfsuc  9836  nominpos  12032  nnunb  12051  indstr  12477  eirr  15729  sqrt2irr  15773  vdwap0  16492  smndex1n0mnd  18293  smndex2dnrinv  18296  psgnunilem3  18842  bwth  22261  zfbas  22747  aaliou3lem9  25197  vma1  26002  hatomistici  30397  esumrnmpt2  31702  fmlan0  33020  linedegen  34131  limsucncmpi  34320  elpadd0  37509  fourierdlem62  43327  etransc  43442  0nodd  44980  2nodd  44982  1neven  45106