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 3779 nfiunxy 3897 nfiinxy 3898 nfiunya 3899 nfiinya 3900 cbviun 3908 cbviin 3909 iunxsngf 3948 cbvdisj 3974 nfdisjv 3976 disjiun 3982 nfmpt 4079 cbvmptf 4081 nffrfor 4331 onintrab2im 4500 tfis 4565 nfxp 4636 opeliunxp 4664 iunxpf 4757 elrnmpt1 4860 fvmptssdm 5578 nfmpo 5919 cbvmpox 5928 fmpox 6176 nffrec 6372 cc3 7217 nfsum1 11306 nfsum 11307 fsum2dlemstep 11384 fisumcom2 11388 nfcprod1 11504 nfcprod 11505 cbvprod 11508 fprod2dlemstep 11572 fprodcom2fi 11576 ctiunctlemudc 12379 ctiunctlemfo 12381 |
Copyright terms: Public domain | W3C validator |