Theorem nrex 3093

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

Syntax hints:  ¬ wn 3   → wi 4   ∈ wcel 2143  ∀wral 3079  ∃wrex 3089

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-ral 3080  df-rex 3090

This theorem is referenced by:  rex0  4316  iun0  5027  canth  7366  orduninsuc  7840  wofib  9508  cfsuc  10242  nominpos  12482  nnunb  12501  indstr  12941  eirr  16262  sqrt2irr  16306  vdwap0  17037  smndex1n0mnd  18975  smndex2dnrinv  18978  psgnunilem3  19567  bwth  23548  zfbas  24034  aaliou3lem9  26492  vma1  27308  muls01  28283  mulsrid  28284  onmulscl  28449  hatomistici  32692  esumrnmpt2  34436  fmlan0  35861  linedegen  36613  limsucncmpi  36934  ttcwf2  37014  mh-inf3sn  37031  elpadd0  40561  rexanuz2nf  46186  fourierdlem62  46862  etransc  46977  cjnpoly  47603  0nodd  48912  2nodd  48914  1neven  48980