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 1412 | . 2 ⊢ (𝜓 → ∀𝑥𝜓) |
3 | sbie.2 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓)) | |
4 | 2, 3 | sbieh 1673 | 1 ⊢ ([𝑦 / 𝑥]𝜑 ↔ 𝜓) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 Ⅎwnf 1349 [wsb 1645 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-i9 1423 ax-ial 1427 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 |
This theorem is referenced by: cbveu 1924 mo4f 1960 bm1.1 2025 eqsb3lem 2140 clelsb3 2142 clelsb4 2143 cbvab 2160 cbvralf 2527 cbvrexf 2528 cbvreu 2531 sbralie 2546 cbvrab 2555 reu2 2729 nfcdeq 2761 sbcco2 2786 sbcie2g 2796 sbcralt 2834 sbcrext 2835 sbcralg 2836 sbcreug 2838 sbcel12g 2865 sbceqg 2866 cbvralcsf 2908 cbvrexcsf 2909 cbvreucsf 2910 cbvrabcsf 2911 sbss 3329 sbcbrg 3813 cbvopab1 3830 cbvmpt 3851 tfis2f 4307 cbviota 4872 relelfvdm 5205 nfvres 5206 cbvriota 5478 |
Copyright terms: Public domain | W3C validator |