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 2271, 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 2272 | . 2 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴) |
3 | 2 | nfi 1438 | 1 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
Colors of variables: wff set class |
Syntax hints: Ⅎwnf 1436 ∈ wcel 1480 Ⅎwnfc 2266 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-nf 1437 df-sb 1736 df-cleq 2130 df-clel 2133 df-nfc 2268 |
This theorem is referenced by: clelsb3f 2283 nfnfc 2286 nfeq 2287 nfel 2288 cleqf 2303 sbabel 2305 r2alf 2450 r2exf 2451 nfrabxy 2609 cbvralf 2646 cbvrexf 2647 cbvrab 2679 rmo3f 2876 nfccdeq 2902 sbcabel 2985 cbvcsbw 3002 cbvcsb 3003 cbvralcsf 3057 cbvrexcsf 3058 cbvreucsf 3059 cbvrabcsf 3060 dfss2f 3083 nfdif 3192 nfun 3227 nfin 3277 nfop 3716 nfiunxy 3834 nfiinxy 3835 nfiunya 3836 nfiinya 3837 cbviun 3845 cbviin 3846 iunxsngf 3885 cbvdisj 3911 nfdisjv 3913 disjiun 3919 nfmpt 4015 cbvmptf 4017 nffrfor 4265 onintrab2im 4429 tfis 4492 nfxp 4561 opeliunxp 4589 iunxpf 4682 elrnmpt1 4785 fvmptssdm 5498 nfmpo 5833 cbvmpox 5842 fmpox 6091 nffrec 6286 nfsum1 11118 nfsum 11119 fsum2dlemstep 11196 fisumcom2 11200 nfcprod1 11316 nfcprod 11317 cbvprod 11320 ctiunctlemudc 11939 ctiunctlemfo 11941 |
Copyright terms: Public domain | W3C validator |