![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbequ12 | GIF version |
Description: An equality theorem for substitution. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sbequ12 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequ1 1699 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
2 | sbequ2 1700 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
3 | 1, 2 | impbid 128 | 1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 [wsb 1693 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-4 1446 |
This theorem depends on definitions: df-bi 116 df-sb 1694 |
This theorem is referenced by: sbequ12r 1703 sbequ12a 1704 sbid 1705 ax16 1742 sb8h 1783 sb8eh 1784 sb8 1785 sb8e 1786 ax16ALT 1788 sbco 1891 sbcomxyyz 1895 sb9v 1903 sb6a 1913 mopick 2027 clelab 2213 sbab 2215 cbvralf 2585 cbvrexf 2586 cbvralsv 2602 cbvrexsv 2603 cbvrab 2618 sbhypf 2669 mob2 2796 reu2 2804 reu6 2805 sbcralt 2916 sbcrext 2917 sbcralg 2918 sbcreug 2920 cbvreucsf 2993 cbvrabcsf 2994 cbvopab1 3917 cbvopab1s 3919 csbopabg 3922 cbvmptf 3938 cbvmpt 3939 opelopabsb 4096 frind 4188 tfis 4411 findes 4431 opeliunxp 4506 ralxpf 4595 rexxpf 4596 cbviota 4998 csbiotag 5021 cbvriota 5632 csbriotag 5634 abrexex2g 5905 opabex3d 5906 opabex3 5907 abrexex2 5909 dfoprab4f 5977 finexdc 6672 ssfirab 6697 uzind4s 9139 zsupcllemstep 11280 bezoutlemmain 11326 cbvrald 11961 bj-bdfindes 12117 bj-findes 12149 |
Copyright terms: Public domain | W3C validator |