Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sbie | Unicode version |
Description: Conversion of implicit substitution to explicit substitution. (Contributed by NM, 30-Jun-1994.) (Revised by Mario Carneiro, 4-Oct-2016.) (Revised by Wolf Lammen, 30-Apr-2018.) |
Ref | Expression |
---|---|
sbie.1 | |
sbie.2 |
Ref | Expression |
---|---|
sbie |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbie.1 | . . 3 | |
2 | 1 | nfri 1517 | . 2 |
3 | sbie.2 | . 2 | |
4 | 2, 3 | sbieh 1788 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 105 wnf 1458 wsb 1760 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1445 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-4 1508 ax-i9 1528 ax-ial 1532 |
This theorem depends on definitions: df-bi 117 df-nf 1459 df-sb 1761 |
This theorem is referenced by: sbiev 1790 cbveu 2048 mo4f 2084 bm1.1 2160 eqsb1lem 2278 clelsb1 2280 clelsb2 2281 cbvab 2299 clelsb1f 2321 cbvralf 2694 cbvrexf 2695 cbvreu 2699 sbralie 2719 cbvrab 2733 reu2 2923 rmo4f 2933 nfcdeq 2957 sbcco2 2983 sbcie2g 2994 sbcralt 3037 sbcrext 3038 sbcralg 3039 sbcreug 3041 sbcel12g 3070 sbceqg 3071 cbvralcsf 3117 cbvrexcsf 3118 cbvreucsf 3119 cbvrabcsf 3120 sbss 3529 disjiun 3993 sbcbrg 4052 cbvopab1 4071 cbvmpt 4093 tfis2f 4577 cbviota 5175 relelfvdm 5539 nfvres 5540 cbvriota 5831 bezoutlemnewy 11963 bezoutlemmain 11965 |
Copyright terms: Public domain | W3C validator |