![]() |
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 1506 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nfi 1473 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1471 ∃wex 1503 |
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 1460 ax-ie1 1504 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: nf3 1680 sb4or 1844 nfmo1 2050 euexex 2123 2moswapdc 2128 nfre1 2533 ceqsexg 2880 morex 2936 sbc6g 3002 rgenm 3540 intab 3888 nfopab1 4087 nfopab2 4088 copsexg 4262 copsex2t 4263 copsex2g 4264 eusv2nf 4474 onintonm 4534 mosubopt 4709 dmcoss 4914 imadif 5315 funimaexglem 5318 nfoprab1 5946 nfoprab2 5947 nfoprab3 5948 exmidfodomrlemr 7232 exmidfodomrlemrALT 7233 dfgrp3mlem 13057 |
Copyright terms: Public domain | W3C validator |