Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfa1 | Unicode version |
Description: is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfa1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | hba1 1505 | . 2 | |
2 | 1 | nfi 1423 | 1 |
Colors of variables: wff set class |
Syntax hints: wal 1314 wnf 1421 |
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-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: nfnf1 1508 nfa2 1543 nfia1 1544 alexdc 1583 nf2 1631 cbv1h 1708 sbf2 1736 sb4or 1789 nfsbxy 1895 nfsbxyt 1896 sbcomxyyz 1923 sbalyz 1952 dvelimALT 1963 nfeu1 1988 moim 2041 euexex 2062 nfaba1 2264 nfra1 2443 ceqsalg 2688 elrab3t 2812 mo2icl 2836 csbie2t 3018 sbcnestgf 3021 dfss4st 3279 dfnfc2 3724 mpteq12f 3978 copsex2t 4137 ssopab2 4167 alxfr 4352 eunex 4446 mosubopt 4574 fv3 5412 fvmptt 5480 fnoprabg 5840 fiintim 6785 bj-exlimmp 12903 bdsepnft 13012 setindft 13090 strcollnft 13109 |
Copyright terms: Public domain | W3C validator |