Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfe1 | Unicode version |
Description: is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfe1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hbe1 1456 | . 2 | |
2 | 1 | nfi 1423 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1421 wex 1453 |
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 1410 ax-ie1 1454 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: nf3 1632 sb4or 1789 nfmo1 1989 euexex 2062 2moswapdc 2067 nfre1 2453 ceqsexg 2787 morex 2841 sbc6g 2906 rgenm 3435 intab 3770 nfopab1 3967 nfopab2 3968 copsexg 4136 copsex2t 4137 copsex2g 4138 eusv2nf 4347 onintonm 4403 mosubopt 4574 dmcoss 4778 imadif 5173 funimaexglem 5176 nfoprab1 5788 nfoprab2 5789 nfoprab3 5790 exmidfodomrlemr 7026 exmidfodomrlemrALT 7027 |
Copyright terms: Public domain | W3C validator |