![]() |
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 1855 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
3 | 1, 2 | mpgbi 1874 | 1 ⊢ ¬ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∃wex 1853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 |
This theorem depends on definitions: df-bi 197 df-ex 1854 |
This theorem is referenced by: ru 3575 axnulALT 4939 notzfaus 4989 dtrucor2 5050 opelopabsb 5135 0nelxp 5300 0nelxpOLD 5301 0xp 5356 dm0 5494 cnv0 5693 co02 5810 dffv3 6348 mpt20 6890 canth2 8278 brdom3 9542 ruc 15171 meet0 17338 join0 17339 0g0 17464 ustn0 22225 bnj1523 31446 linedegen 32556 nextnt 32710 nextf 32711 unqsym1 32730 amosym1 32731 subsym1 32732 bj-dtrucor2v 33107 bj-ru1 33239 bj-0nelsngl 33265 bj-ccinftydisj 33411 |
Copyright terms: Public domain | W3C validator |