Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfcri | Unicode version |
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2304, this does not require and to be disjoint.) (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfcri.1 |
Ref | Expression |
---|---|
nfcri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcri.1 | . . 3 | |
2 | 1 | nfcrii 2305 | . 2 |
3 | 2 | nfi 1455 | 1 |
Colors of variables: wff set class |
Syntax hints: wnf 1453 wcel 2141 wnfc 2299 |
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-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-nf 1454 df-sb 1756 df-cleq 2163 df-clel 2166 df-nfc 2301 |
This theorem is referenced by: clelsb1f 2316 nfnfc 2319 nfeq 2320 nfel 2321 cleqf 2337 sbabel 2339 r2alf 2487 r2exf 2488 nfrabxy 2650 cbvralfw 2687 cbvrexfw 2688 cbvralf 2689 cbvrexf 2690 cbvrab 2728 rmo3f 2927 nfccdeq 2953 sbcabel 3036 cbvcsbw 3053 cbvcsb 3054 cbvralcsf 3111 cbvrexcsf 3112 cbvreucsf 3113 cbvrabcsf 3114 dfss2f 3138 nfdif 3248 nfun 3283 nfin 3333 nfop 3781 nfiunxy 3899 nfiinxy 3900 nfiunya 3901 nfiinya 3902 cbviun 3910 cbviin 3911 iunxsngf 3950 cbvdisj 3976 nfdisjv 3978 disjiun 3984 nfmpt 4081 cbvmptf 4083 nffrfor 4333 onintrab2im 4502 tfis 4567 nfxp 4638 opeliunxp 4666 iunxpf 4759 elrnmpt1 4862 fvmptssdm 5580 nfmpo 5922 cbvmpox 5931 fmpox 6179 nffrec 6375 cc3 7230 nfsum1 11319 nfsum 11320 fsum2dlemstep 11397 fisumcom2 11401 nfcprod1 11517 nfcprod 11518 cbvprod 11521 fprod2dlemstep 11585 fprodcom2fi 11589 ctiunctlemudc 12392 ctiunctlemfo 12394 |
Copyright terms: Public domain | W3C validator |