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 1741 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
2 | sbequ2 1742 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
3 | 1, 2 | impbid 128 | 1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 [wsb 1735 |
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-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 |
This theorem depends on definitions: df-bi 116 df-sb 1736 |
This theorem is referenced by: sbequ12r 1745 sbequ12a 1746 sbid 1747 ax16 1785 sb8h 1826 sb8eh 1827 sb8 1828 sb8e 1829 ax16ALT 1831 sbco 1941 sbcomxyyz 1945 sb9v 1953 sb6a 1963 mopick 2077 clelab 2265 sbab 2267 cbvralf 2648 cbvrexf 2649 cbvralsv 2668 cbvrexsv 2669 cbvrab 2684 sbhypf 2735 mob2 2864 reu2 2872 reu6 2873 sbcralt 2985 sbcrext 2986 sbcralg 2987 sbcreug 2989 cbvreucsf 3064 cbvrabcsf 3065 cbvopab1 4001 cbvopab1s 4003 csbopabg 4006 cbvmptf 4022 cbvmpt 4023 opelopabsb 4182 frind 4274 tfis 4497 findes 4517 opeliunxp 4594 ralxpf 4685 rexxpf 4686 cbviota 5093 csbiotag 5116 cbvriota 5740 csbriotag 5742 abrexex2g 6018 opabex3d 6019 opabex3 6020 abrexex2 6022 dfoprab4f 6091 finexdc 6796 ssfirab 6822 uzind4s 9385 zsupcllemstep 11638 bezoutlemmain 11686 cbvrald 12995 bj-bdfindes 13147 bj-findes 13179 |
Copyright terms: Public domain | W3C validator |