Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfal | Unicode version |
Description: If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfal.1 |
Ref | Expression |
---|---|
nfal |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfal.1 | . . . 4 | |
2 | 1 | nfri 1499 | . . 3 |
3 | 2 | hbal 1453 | . 2 |
4 | 3 | nfi 1438 | 1 |
Colors of variables: wff set class |
Syntax hints: wal 1329 wnf 1436 |
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-5 1423 ax-7 1424 ax-gen 1425 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-nf 1437 |
This theorem is referenced by: nfnf 1556 nfa2 1558 aaan 1566 cbv3 1720 cbv2 1725 nfald 1733 cbval2 1891 nfsb4t 1987 nfeuv 2015 mo23 2038 bm1.1 2122 nfnfc1 2282 nfnfc 2286 nfeq 2287 sbcnestgf 3046 dfnfc2 3749 nfdisjv 3913 nfdisj1 3914 nffr 4266 exmidfodomrlemr 7051 exmidfodomrlemrALT 7052 exmidunben 11928 bdsepnft 13074 bdsepnfALT 13076 setindft 13152 strcollnft 13171 strcollnfALT 13173 |
Copyright terms: Public domain | W3C validator |