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 1697 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
3 | 1, 2 | mpgbi 1716 | 1 ⊢ ¬ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∃wex 1695 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 |
This theorem depends on definitions: df-bi 196 df-ex 1696 |
This theorem is referenced by: ru 3401 axnulALT 4715 notzfaus 4766 dtrucor2 4828 opelopabsb 4910 0nelxp 5067 0nelxpOLD 5068 0xp 5122 dm0 5260 cnv0 5454 co02 5566 dffv3 6099 mpt20 6623 canth2 7998 brdom3 9231 ruc 14811 meet0 16960 join0 16961 0g0 17086 ustn0 21834 bnj1523 30393 linedegen 31420 nextnt 31574 nextf 31575 unqsym1 31594 amosym1 31595 subsym1 31596 bj-dtrucor2v 31989 bj-ru1 32125 bj-0nelsngl 32152 bj-ccinftydisj 32277 |
Copyright terms: Public domain | W3C validator |