![]() |
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 1453 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
3 | sbie.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | sbieh 1714 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 Ⅎwnf 1390 [wsb 1686 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-5 1377 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-4 1441 ax-i9 1464 ax-ial 1468 |
This theorem depends on definitions: df-bi 115 df-nf 1391 df-sb 1687 |
This theorem is referenced by: cbveu 1966 mo4f 2002 bm1.1 2067 eqsb3lem 2182 clelsb3 2184 clelsb4 2185 cbvab 2202 cbvralf 2572 cbvrexf 2573 cbvreu 2576 sbralie 2591 cbvrab 2600 reu2 2781 nfcdeq 2813 sbcco2 2838 sbcie2g 2848 sbcralt 2891 sbcrext 2892 sbcralg 2893 sbcreug 2895 sbcel12g 2922 sbceqg 2923 cbvralcsf 2965 cbvrexcsf 2966 cbvreucsf 2967 cbvrabcsf 2968 sbss 3357 sbcbrg 3842 cbvopab1 3859 cbvmpt 3880 tfis2f 4333 cbviota 4902 relelfvdm 5237 nfvres 5238 cbvriota 5509 bezoutlemnewy 10529 bezoutlemmain 10531 |
Copyright terms: Public domain | W3C validator |