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 1787 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
3 | 1, 2 | mpgbi 1804 | 1 ⊢ ¬ ∃𝑥𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∃wex 1785 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 |
This theorem depends on definitions: df-bi 206 df-ex 1786 |
This theorem is referenced by: ru 3718 noel 4269 noelOLD 4270 axnulALT 5231 notzfaus 5288 dtrucor2 5298 opelopabsb 5444 0nelopab 5479 0nelxp 5622 0xp 5683 dm0 5826 cnv0 6041 co02 6161 dffv3 6764 mpo0 7351 canth2 8882 brdom3 10268 ruc 15933 join0 18104 meet0 18105 0g0 18329 ustn0 23353 bnj1523 33030 linedegen 34424 nexntru 34572 nexfal 34573 unqsym1 34593 amosym1 34594 subsym1 34595 bj-dtrucor2v 34979 bj-ru1 35111 bj-0nelsngl 35140 bj-ccinftydisj 35363 disjALTV0 36841 dtrucor3 46096 |
Copyright terms: Public domain | W3C validator |