![]() |
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 1480 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | sbie.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | sbieh 1744 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-i9 1491 ax-ial 1495 |
This theorem depends on definitions: df-bi 116 df-nf 1418 df-sb 1717 |
This theorem is referenced by: cbveu 1997 mo4f 2033 bm1.1 2098 eqsb3lem 2215 clelsb3 2217 clelsb4 2218 cbvab 2235 clelsb3f 2257 cbvralf 2620 cbvrexf 2621 cbvreu 2624 sbralie 2639 cbvrab 2653 reu2 2839 rmo4f 2849 nfcdeq 2873 sbcco2 2898 sbcie2g 2908 sbcralt 2951 sbcrext 2952 sbcralg 2953 sbcreug 2955 sbcel12g 2982 sbceqg 2983 cbvralcsf 3026 cbvrexcsf 3027 cbvreucsf 3028 cbvrabcsf 3029 sbss 3435 disjiun 3888 sbcbrg 3942 cbvopab1 3959 cbvmpt 3981 tfis2f 4456 cbviota 5049 relelfvdm 5405 nfvres 5406 cbvriota 5692 bezoutlemnewy 11524 bezoutlemmain 11526 |
Copyright terms: Public domain | W3C validator |