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 1482 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nfi 1449 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1447 ∃wex 1479 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1436 ax-ie1 1480 |
This theorem depends on definitions: df-bi 116 df-nf 1448 |
This theorem is referenced by: nf3 1656 sb4or 1820 nfmo1 2025 euexex 2098 2moswapdc 2103 nfre1 2507 ceqsexg 2849 morex 2905 sbc6g 2970 rgenm 3506 intab 3847 nfopab1 4045 nfopab2 4046 copsexg 4216 copsex2t 4217 copsex2g 4218 eusv2nf 4428 onintonm 4488 mosubopt 4663 dmcoss 4867 imadif 5262 funimaexglem 5265 nfoprab1 5882 nfoprab2 5883 nfoprab3 5884 exmidfodomrlemr 7149 exmidfodomrlemrALT 7150 |
Copyright terms: Public domain | W3C validator |