| 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 1781 | . 2 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑) | |
| 2 | nex.1 | . 2 ⊢ ¬ 𝜑 | |
| 3 | 1, 2 | mpgbi 1798 | 1 ⊢ ¬ ∃𝑥𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 ∃wex 1779 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 |
| This theorem depends on definitions: df-bi 207 df-ex 1780 |
| This theorem is referenced by: ru 3786 ruOLD 3787 noel 4338 axnulALT 5304 notzfaus 5363 dtrucor2 5372 opelopabsb 5535 0nelopab 5572 0nelxp 5719 0xp 5784 dm0 5931 cnv0 6160 co02 6280 dffv3 6902 mpo0 7518 canth2 9170 snnen2o 9273 1sdom2dom 9283 brdom3 10568 ruc 16279 join0 18450 meet0 18451 0g0 18677 ustn0 24229 bnj1523 35085 linedegen 36144 nexntru 36405 nexfal 36406 unqsym1 36426 bj-dtrucor2v 36818 bj-ru1 36944 bj-0nelsngl 36972 bj-ccinftydisj 37214 disjALTV0 38755 dtrucor3 48719 |
| Copyright terms: Public domain | W3C validator |