![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nex | Structured version Visualization version GIF version |
Description: Generalization rule for negated wff. (Contributed by NM, 18-May-1994.) |
Ref | Expression |
---|---|
nex.1 | ⊢ ¬ 𝜑 |
Ref | Expression |
---|---|
nex | ⊢ ¬ ∃𝑥𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | alnex 1825 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
3 | 1, 2 | mpgbi 1842 | 1 ⊢ ¬ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∃wex 1823 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: ru 3650 noel 4145 axnulALT 5023 notzfaus 5074 dtrucor2 5084 opelopabsb 5222 0nelxp 5389 0xp 5447 dm0 5584 cnv0 5790 co02 5903 dffv3 6442 mpt20 7002 canth2 8401 brdom3 9685 ruc 15376 meet0 17523 join0 17524 0g0 17649 ustn0 22432 bnj1523 31738 linedegen 32839 nexntru 32987 nexfal 32988 unqsym1 33007 amosym1 33008 subsym1 33009 bj-dtrucor2v 33377 bj-ru1 33506 bj-0nelsngl 33531 bj-ccinftydisj 33690 nsb 38102 |
Copyright terms: Public domain | W3C validator |