![]() |
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 2274, 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 2275 | . 2 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
3 | 2 | nfi 1439 | 1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1437 ∈ wcel 1481 Ⅎwnfc 2269 |
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 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-10 1484 ax-11 1485 ax-i12 1486 ax-bndl 1487 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-cleq 2133 df-clel 2136 df-nfc 2271 |
This theorem is referenced by: clelsb3f 2286 nfnfc 2289 nfeq 2290 nfel 2291 cleqf 2306 sbabel 2308 r2alf 2455 r2exf 2456 nfrabxy 2614 cbvralf 2651 cbvrexf 2652 cbvrab 2687 rmo3f 2885 nfccdeq 2911 sbcabel 2994 cbvcsbw 3011 cbvcsb 3012 cbvralcsf 3067 cbvrexcsf 3068 cbvreucsf 3069 cbvrabcsf 3070 dfss2f 3093 nfdif 3202 nfun 3237 nfin 3287 nfop 3729 nfiunxy 3847 nfiinxy 3848 nfiunya 3849 nfiinya 3850 cbviun 3858 cbviin 3859 iunxsngf 3898 cbvdisj 3924 nfdisjv 3926 disjiun 3932 nfmpt 4028 cbvmptf 4030 nffrfor 4278 onintrab2im 4442 tfis 4505 nfxp 4574 opeliunxp 4602 iunxpf 4695 elrnmpt1 4798 fvmptssdm 5513 nfmpo 5848 cbvmpox 5857 fmpox 6106 nffrec 6301 cc3 7100 nfsum1 11157 nfsum 11158 fsum2dlemstep 11235 fisumcom2 11239 nfcprod1 11355 nfcprod 11356 cbvprod 11359 ctiunctlemudc 11986 ctiunctlemfo 11988 |
Copyright terms: Public domain | W3C validator |