Theorem nrex 3058

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2109  ∀wral 3045  ∃wrex 3054

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-ral 3046  df-rex 3055

This theorem is referenced by:  rex0  4326  iun0  5029  canth  7344  orduninsuc  7822  wofib  9505  cfsuc  10217  nominpos  12426  nnunb  12445  indstr  12882  eirr  16180  sqrt2irr  16224  vdwap0  16954  smndex1n0mnd  18846  smndex2dnrinv  18849  psgnunilem3  19433  bwth  23304  zfbas  23790  aaliou3lem9  26265  vma1  27083  muls01  28022  mulsrid  28023  onmulscl  28182  hatomistici  32298  esumrnmpt2  34065  fmlan0  35385  linedegen  36138  limsucncmpi  36440  elpadd0  39810  rexanuz2nf  45495  fourierdlem62  46173  etransc  46288  0nodd  48162  2nodd  48164  1neven  48230