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 1651 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
2 | sbequ2 1652 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
3 | 1, 2 | impbid 120 | 1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 [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-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 |
This theorem depends on definitions: df-bi 110 df-sb 1646 |
This theorem is referenced by: sbequ12r 1655 sbequ12a 1656 sbid 1657 ax16 1694 sb8h 1734 sb8eh 1735 sb8 1736 sb8e 1737 ax16ALT 1739 sbco 1842 sbcomxyyz 1846 sb9v 1854 sb6a 1864 mopick 1978 clelab 2162 sbab 2164 cbvralf 2527 cbvrexf 2528 cbvralsv 2544 cbvrexsv 2545 cbvrab 2555 sbhypf 2603 mob2 2721 reu2 2729 reu6 2730 sbcralt 2834 sbcrext 2835 sbcralg 2836 sbcreug 2838 cbvreucsf 2910 cbvrabcsf 2911 cbvopab1 3830 cbvopab1s 3832 csbopabg 3835 cbvmpt 3851 opelopabsb 3997 frind 4089 tfis 4306 findes 4326 opeliunxp 4395 ralxpf 4482 rexxpf 4483 cbviota 4872 csbiotag 4895 cbvriota 5478 csbriotag 5480 abrexex2g 5747 opabex3d 5748 opabex3 5749 abrexex2 5751 dfoprab4f 5819 uzind4s 8533 cbvrald 9927 bj-bdfindes 10074 bj-findes 10106 |
Copyright terms: Public domain | W3C validator |