![]() |
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 1854 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
3 | 1, 2 | mpgbi 1873 | 1 ⊢ ¬ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∃wex 1852 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 |
This theorem depends on definitions: df-bi 197 df-ex 1853 |
This theorem is referenced by: ru 3586 axnulALT 4921 notzfaus 4971 dtrucor2 5029 opelopabsb 5118 0nelxp 5283 0nelxpOLD 5284 0xp 5339 dm0 5477 cnv0 5676 co02 5793 dffv3 6328 mpt20 6872 canth2 8269 brdom3 9552 ruc 15178 meet0 17345 join0 17346 0g0 17471 ustn0 22244 bnj1523 31477 linedegen 32587 nextnt 32741 nextf 32742 unqsym1 32761 amosym1 32762 subsym1 32763 bj-dtrucor2v 33137 bj-ru1 33265 bj-0nelsngl 33290 bj-ccinftydisj 33437 |
Copyright terms: Public domain | W3C validator |