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 2145  ∀wral 3079  ∃wrex 3089

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

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

This theorem is referenced by:  rex0  4316  iun0  5022  canth  7354  orduninsuc  7827  wofib  9495  cfsuc  10229  nominpos  12472  nnunb  12491  indstr  12931  eirr  16251  sqrt2irr  16295  vdwap0  17026  smndex1n0mnd  18964  smndex2dnrinv  18967  psgnunilem3  19557  bwth  23528  zfbas  24014  aaliou3lem9  26472  vma1  27288  muls01  28263  mulsrid  28264  onmulscl  28429  hatomistici  32623  esumrnmpt2  34375  fmlan0  35754  linedegen  36506  limsucncmpi  36818  ttcwf2  36898  mh-inf3sn  36915  elpadd0  40445  rexanuz2nf  46064  fourierdlem62  46740  etransc  46855  cjnpoly  47481  0nodd  48790  2nodd  48792  1neven  48858