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 3061 | . 2 ⊢ ∀𝑥 ∈ 𝐴 ¬ 𝜓 |
3 | ralnex 3148 | . 2 ⊢ (∀𝑥 ∈ 𝐴 ¬ 𝜓 ↔ ¬ ∃𝑥 ∈ 𝐴 𝜓) | |
4 | 2, 3 | mpbi 233 | 1 ⊢ ¬ ∃𝑥 ∈ 𝐴 𝜓 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∈ wcel 2112 ∀wral 3051 ∃wrex 3052 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-ral 3056 df-rex 3057 |
This theorem is referenced by: rex0 4258 iun0 4956 canth 7145 orduninsuc 7600 wfrlem16 8048 wofib 9139 cfsuc 9836 nominpos 12032 nnunb 12051 indstr 12477 eirr 15729 sqrt2irr 15773 vdwap0 16492 smndex1n0mnd 18293 smndex2dnrinv 18296 psgnunilem3 18842 bwth 22261 zfbas 22747 aaliou3lem9 25197 vma1 26002 hatomistici 30397 esumrnmpt2 31702 fmlan0 33020 linedegen 34131 limsucncmpi 34320 elpadd0 37509 fourierdlem62 43327 etransc 43442 0nodd 44980 2nodd 44982 1neven 45106 |
Copyright terms: Public domain | W3C validator |