| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > nfe1 | GIF version | ||
| Description: 𝑥 is not free in ∃𝑥𝜑. (Contributed by Mario Carneiro, 11-Aug-2016.) |
| Ref | Expression |
|---|---|
| nfe1 | ⊢ Ⅎ𝑥∃𝑥𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hbe1 1517 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
| 2 | 1 | nfi 1484 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
| Colors of variables: wff set class |
| Syntax hints: Ⅎwnf 1482 ∃wex 1514 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-gen 1471 ax-ie1 1515 |
| This theorem depends on definitions: df-bi 117 df-nf 1483 |
| This theorem is referenced by: nf3 1691 sb4or 1855 nfmo1 2065 euexex 2138 2moswapdc 2143 nfre1 2548 ceqsexg 2900 morex 2956 sbc6g 3022 intab 3913 nfopab1 4112 nfopab2 4113 copsexg 4287 copsex2t 4288 copsex2g 4289 eusv2nf 4501 onintonm 4563 mosubopt 4738 dmcoss 4945 imadif 5348 funimaexglem 5351 nfoprab1 5984 nfoprab2 5985 nfoprab3 5986 exmidfodomrlemr 7292 exmidfodomrlemrALT 7293 dfgrp3mlem 13348 |
| Copyright terms: Public domain | W3C validator |