Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nfcri | GIF version |
Description: Consequence of the not-free predicate. (Note that unlike nfcr 2250, 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 2251 | . 2 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
3 | 2 | nfi 1423 | 1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1421 ∈ wcel 1465 Ⅎwnfc 2245 |
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 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-cleq 2110 df-clel 2113 df-nfc 2247 |
This theorem is referenced by: clelsb3f 2262 nfnfc 2265 nfeq 2266 nfel 2267 cleqf 2282 sbabel 2284 r2alf 2429 r2exf 2430 nfrabxy 2588 cbvralf 2625 cbvrexf 2626 cbvrab 2658 rmo3f 2854 nfccdeq 2880 sbcabel 2962 cbvcsb 2979 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 cbvrabcsf 3035 dfss2f 3058 nfdif 3167 nfun 3202 nfin 3252 nfop 3691 nfiunxy 3809 nfiinxy 3810 nfiunya 3811 nfiinya 3812 cbviun 3820 cbviin 3821 iunxsngf 3860 cbvdisj 3886 nfdisjv 3888 disjiun 3894 nfmpt 3990 cbvmptf 3992 nffrfor 4240 onintrab2im 4404 tfis 4467 nfxp 4536 opeliunxp 4564 iunxpf 4657 elrnmpt1 4760 fvmptssdm 5473 nfmpo 5808 cbvmpox 5817 fmpox 6066 nffrec 6261 nfsum1 11093 nfsum 11094 fsum2dlemstep 11171 fisumcom2 11175 ctiunctlemudc 11877 ctiunctlemfo 11879 |
Copyright terms: Public domain | W3C validator |