![]() |
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 1776 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
3 | 1, 2 | mpgbi 1793 | 1 ⊢ ¬ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∃wex 1774 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 |
This theorem depends on definitions: df-bi 206 df-ex 1775 |
This theorem is referenced by: ru 3773 ruOLD 3774 noel 4330 noelOLD 4331 axnulALT 5301 notzfaus 5359 dtrucor2 5368 opelopabsb 5528 0nelopab 5565 0nelxp 5708 0xp 5772 dm0 5919 cnv0 6144 co02 6263 dffv3 6889 mpo0 7502 canth2 9160 snnen2o 9264 1sdom2dom 9274 brdom3 10562 ruc 16240 join0 18425 meet0 18426 0g0 18652 ustn0 24213 bnj1523 34929 linedegen 35980 nexntru 36129 nexfal 36130 unqsym1 36150 bj-dtrucor2v 36535 bj-ru1 36663 bj-0nelsngl 36691 bj-ccinftydisj 36933 disjALTV0 38465 dtrucor3 48222 |
Copyright terms: Public domain | W3C validator |