Theorem nrex 3094

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-ral 3081  df-rex 3091

This theorem is used by:  rex0  4311  iun0  5023  canth  7397  orduninsuc  7878  wofib  9566  cfsuc  10362  nominpos  12610  nnunb  12629  indstr  13070  eirr  16402  sqrt2irr  16446  vdwap0  17183  smndex1n0mnd  19140  smndex2dnrinv  19143  psgnunilem3  19740  bwth  23758  zfbas  24245  aaliou3lem9  26707  vma1  27523  muls01  28528  mulsrid  28529  onmulscl  28694  hatomistici  32994  esumrnmpt2  34770  fmlan0  36323  linedegen  37086  limsucncmpi  37411  ttcwf2  37491  mh-inf3sn  37508  elpadd0  41058  rexanuz2nf  46707  fourierdlem62  47383  etransc  47498  cjnpoly  48144  0nodd  49472  2nodd  49474  1neven  49540