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 1484 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
3 | sbie.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | sbieh 1748 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 Ⅎwnf 1421 [wsb 1720 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-i9 1495 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 |
This theorem is referenced by: cbveu 2001 mo4f 2037 bm1.1 2102 eqsb3lem 2220 clelsb3 2222 clelsb4 2223 cbvab 2240 clelsb3f 2262 cbvralf 2625 cbvrexf 2626 cbvreu 2629 sbralie 2644 cbvrab 2658 reu2 2845 rmo4f 2855 nfcdeq 2879 sbcco2 2904 sbcie2g 2914 sbcralt 2957 sbcrext 2958 sbcralg 2959 sbcreug 2961 sbcel12g 2988 sbceqg 2989 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 cbvrabcsf 3035 sbss 3441 disjiun 3894 sbcbrg 3952 cbvopab1 3971 cbvmpt 3993 tfis2f 4468 cbviota 5063 relelfvdm 5421 nfvres 5422 cbvriota 5708 bezoutlemnewy 11611 bezoutlemmain 11613 |
Copyright terms: Public domain | W3C validator |