![]() |
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 1439 | . 2 ⊢ (∃𝑥𝜑 → ∀𝑥∃𝑥𝜑) | |
2 | 1 | nfi 1406 | 1 ⊢ Ⅎ𝑥∃𝑥𝜑 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1404 ∃wex 1436 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1393 ax-ie1 1437 |
This theorem depends on definitions: df-bi 116 df-nf 1405 |
This theorem is referenced by: nf3 1615 sb4or 1772 nfmo1 1972 euexex 2045 2moswapdc 2050 nfre1 2435 ceqsexg 2767 morex 2821 sbc6g 2886 rgenm 3412 intab 3747 nfopab1 3937 nfopab2 3938 copsexg 4104 copsex2t 4105 copsex2g 4106 eusv2nf 4315 onintonm 4371 mosubopt 4542 dmcoss 4744 imadif 5139 funimaexglem 5142 nfoprab1 5752 nfoprab2 5753 nfoprab3 5754 exmidfodomrlemr 6967 exmidfodomrlemrALT 6968 |
Copyright terms: Public domain | W3C validator |