![]() |
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 1495 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nfi 1462 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1460 ∃wex 1492 |
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 1449 ax-ie1 1493 |
This theorem depends on definitions: df-bi 117 df-nf 1461 |
This theorem is referenced by: nf3 1669 sb4or 1833 nfmo1 2038 euexex 2111 2moswapdc 2116 nfre1 2520 ceqsexg 2865 morex 2921 sbc6g 2987 rgenm 3525 intab 3871 nfopab1 4069 nfopab2 4070 copsexg 4241 copsex2t 4242 copsex2g 4243 eusv2nf 4453 onintonm 4513 mosubopt 4688 dmcoss 4892 imadif 5292 funimaexglem 5295 nfoprab1 5918 nfoprab2 5919 nfoprab3 5920 exmidfodomrlemr 7195 exmidfodomrlemrALT 7196 dfgrp3mlem 12854 |
Copyright terms: Public domain | W3C validator |