![]() |
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 1409 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sbie.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sbieh 1670 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-i9 1420 ax-ial 1424 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-sb 1643 |
This theorem is referenced by: cbveu 1921 mo4f 1957 bm1.1 2022 eqsb3lem 2137 clelsb3 2139 clelsb4 2140 cbvab 2157 cbvralf 2521 cbvrexf 2522 cbvreu 2525 sbralie 2540 cbvrab 2549 reu2 2723 nfcdeq 2755 sbcco2 2780 sbcie2g 2790 sbcralt 2828 sbcrext 2829 sbcralg 2830 sbcrexg 2831 sbcreug 2832 sbcel12g 2859 sbceqg 2860 cbvralcsf 2902 cbvrexcsf 2903 cbvreucsf 2904 cbvrabcsf 2905 sbss 3323 sbcbrg 3804 cbvopab1 3821 cbvmpt 3842 tfis2f 4250 cbviota 4815 relelfvdm 5148 nfvres 5149 cbvriota 5421 |
Copyright terms: Public domain | W3C validator |