![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbie | GIF 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 1530 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
3 | sbie.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | sbieh 1801 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 Ⅎwnf 1471 [wsb 1773 |
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 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-i9 1541 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 |
This theorem is referenced by: sbiev 1803 cbveu 2062 mo4f 2098 bm1.1 2174 eqsb1lem 2292 clelsb1 2294 clelsb2 2295 cbvab 2313 clelsb1f 2336 cbvralf 2710 cbvrexf 2711 cbvreu 2716 sbralie 2736 cbvrab 2750 reu2 2940 rmo4f 2950 nfcdeq 2974 sbcco2 3000 sbcie2g 3011 sbcralt 3054 sbcrext 3055 sbcralg 3056 sbcreug 3058 sbcel12g 3087 sbceqg 3088 cbvralcsf 3134 cbvrexcsf 3135 cbvreucsf 3136 cbvrabcsf 3137 sbss 3546 disjiun 4013 sbcbrg 4072 cbvopab1 4091 cbvmpt 4113 tfis2f 4601 cbviota 5201 relelfvdm 5566 nfvres 5568 cbvriota 5863 bezoutlemnewy 12032 bezoutlemmain 12034 |
Copyright terms: Public domain | W3C validator |