Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nrex | Structured version Visualization version GIF version |
Description: Inference adding restricted existential quantifier to negated wff. (Contributed by NM, 16-Oct-2003.) |
Ref | Expression |
---|---|
nrex.1 | ⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) |
Ref | Expression |
---|---|
nrex | ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nrex.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → ¬ 𝜓) | |
2 | 1 | rgen 3148 | . 2 ⊢ ∀𝑥 ∈ 𝐴 ¬ 𝜓 |
3 | ralnex 3236 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbi 232 | 1 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2110 ∀wral 3138 ∃wrex 3139 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1777 df-ral 3143 df-rex 3144 |
This theorem is referenced by: rex0 4316 iun0 4977 canth 7105 orduninsuc 7552 wfrlem16 7964 wofib 9003 cfsuc 9673 nominpos 11868 nnunb 11887 indstr 12310 eirr 15552 sqrt2irr 15596 vdwap0 16306 smndex1n0mnd 18071 smndex2dnrinv 18074 psgnunilem3 18618 bwth 22012 zfbas 22498 aaliou3lem9 24933 vma1 25737 hatomistici 30133 esumrnmpt2 31322 fmlan0 32633 linedegen 33599 limsucncmpi 33788 elpadd0 36939 fourierdlem62 42447 etransc 42562 0nodd 44071 2nodd 44073 1neven 44197 |
Copyright terms: Public domain | W3C validator |