![]() |
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 1500 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
3 | sbie.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | sbieh 1764 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 Ⅎwnf 1437 [wsb 1736 |
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-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-i9 1511 ax-ial 1515 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 |
This theorem is referenced by: sbiev 1766 cbveu 2024 mo4f 2060 bm1.1 2125 eqsb3lem 2243 clelsb3 2245 clelsb4 2246 cbvab 2264 clelsb3f 2286 cbvralf 2651 cbvrexf 2652 cbvreu 2655 sbralie 2673 cbvrab 2687 reu2 2876 rmo4f 2886 nfcdeq 2910 sbcco2 2935 sbcie2g 2946 sbcralt 2989 sbcrext 2990 sbcralg 2991 sbcreug 2993 sbcel12g 3022 sbceqg 3023 cbvralcsf 3067 cbvrexcsf 3068 cbvreucsf 3069 cbvrabcsf 3070 sbss 3476 disjiun 3932 sbcbrg 3990 cbvopab1 4009 cbvmpt 4031 tfis2f 4506 cbviota 5101 relelfvdm 5461 nfvres 5462 cbvriota 5748 bezoutlemnewy 11720 bezoutlemmain 11722 |
Copyright terms: Public domain | W3C validator |