Theorem nrex 3066

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

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

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-ral 3053  df-rex 3063

This theorem is referenced by:  rex0  4301  iun0  5005  canth  7314  orduninsuc  7787  wofib  9453  cfsuc  10170  nominpos  12405  nnunb  12424  indstr  12857  eirr  16163  sqrt2irr  16207  vdwap0  16938  smndex1n0mnd  18874  smndex2dnrinv  18877  psgnunilem3  19462  bwth  23385  zfbas  23871  aaliou3lem9  26327  vma1  27143  muls01  28118  mulsrid  28119  onmulscl  28284  hatomistici  32448  esumrnmpt2  34228  fmlan0  35589  linedegen  36341  limsucncmpi  36643  ttcwf2  36723  mh-inf3sn  36740  elpadd0  40269  rexanuz2nf  45938  fourierdlem62  46614  etransc  46729  cjnpoly  47349  0nodd  48658  2nodd  48660  1neven  48726