Metamath Proof Explorer
Description: Inference adding restricted existential quantifier to negated wff.
(Contributed by NM, 16-Oct-2003)
|
|
Ref |
Expression |
|
Hypothesis |
nrex.1 |
⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜓 ) |
|
Assertion |
nrex |
⊢ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nrex.1 |
⊢ ( 𝑥 ∈ 𝐴 → ¬ 𝜓 ) |
2 |
1
|
rgen |
⊢ ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 |
3 |
|
ralnex |
⊢ ( ∀ 𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 ) |
4 |
2 3
|
mpbi |
⊢ ¬ ∃ 𝑥 ∈ 𝐴 𝜓 |