![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sbequ | GIF version |
Description: An equality theorem for substitution. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequi 1778 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | |
2 | sbequi 1778 | . . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) | |
3 | 2 | equcoms 1652 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) |
4 | 1, 3 | impbid 128 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 [wsb 1703 |
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-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 |
This theorem depends on definitions: df-bi 116 df-nf 1405 df-sb 1704 |
This theorem is referenced by: drsb2 1780 sbco2vlem 1880 sbco2yz 1897 sbcocom 1904 sb10f 1931 hbsb4 1948 nfsb4or 1959 sb8eu 1973 sb8euh 1983 cbvab 2222 cbvralf 2606 cbvrexf 2607 cbvreu 2610 cbvralsv 2623 cbvrexsv 2624 cbvrab 2639 cbvreucsf 3014 cbvrabcsf 3015 sbss 3418 disjiun 3870 cbvopab1 3941 cbvmpt 3963 tfis 4435 findes 4455 cbviota 5029 sb8iota 5031 cbvriota 5672 uzind4s 9235 bezoutlemmain 11479 cbvrald 12576 setindft 12748 |
Copyright terms: Public domain | W3C validator |