![]() |
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 1519 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
3 | sbie.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | sbieh 1790 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 Ⅎwnf 1460 [wsb 1762 |
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 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-i9 1530 ax-ial 1534 |
This theorem depends on definitions: df-bi 117 df-nf 1461 df-sb 1763 |
This theorem is referenced by: sbiev 1792 cbveu 2050 mo4f 2086 bm1.1 2162 eqsb1lem 2280 clelsb1 2282 clelsb2 2283 cbvab 2301 clelsb1f 2323 cbvralf 2696 cbvrexf 2697 cbvreu 2701 sbralie 2721 cbvrab 2735 reu2 2925 rmo4f 2935 nfcdeq 2959 sbcco2 2985 sbcie2g 2996 sbcralt 3039 sbcrext 3040 sbcralg 3041 sbcreug 3043 sbcel12g 3072 sbceqg 3073 cbvralcsf 3119 cbvrexcsf 3120 cbvreucsf 3121 cbvrabcsf 3122 sbss 3531 disjiun 3998 sbcbrg 4057 cbvopab1 4076 cbvmpt 4098 tfis2f 4583 cbviota 5183 relelfvdm 5547 nfvres 5548 cbvriota 5840 bezoutlemnewy 11996 bezoutlemmain 11998 |
Copyright terms: Public domain | W3C validator |