![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbequ12 | Structured version Visualization version GIF version |
Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
sbequ12 | ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequ1 2266 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
2 | sbequ2 2051 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
3 | 1, 2 | impbid 202 | 1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 [wsb 2049 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-12 2203 |
This theorem depends on definitions: df-bi 197 df-an 383 df-ex 1853 df-sb 2050 |
This theorem is referenced by: sbequ12r 2268 sbequ12a 2269 axc16ALT 2513 nfsb4t 2536 sbco2 2562 sb8 2571 sb8e 2572 sbal1 2608 clelab 2897 sbab 2899 cbvralf 3314 cbvralsv 3331 cbvrexsv 3332 cbvrab 3348 sbhypf 3405 mob2 3538 reu2 3546 reu6 3547 sbcralt 3660 sbcreu 3664 cbvreucsf 3716 cbvrabcsf 3717 csbif 4277 cbvopab1 4857 cbvopab1s 4859 cbvmptf 4882 cbvmpt 4883 opelopabsb 5118 csbopab 5141 csbopabgALT 5142 opeliunxp 5310 ralxpf 5407 cbviota 5999 csbiota 6024 f1ossf1o 6538 cbvriota 6764 csbriota 6766 onminex 7154 tfis 7201 findes 7243 abrexex2g 7291 opabex3d 7292 opabex3 7293 abrexex2OLD 7297 dfoprab4f 7375 uzind4s 11950 ac6sf2 29769 esumcvg 30488 bj-sbab 33120 wl-sb8t 33668 wl-sbalnae 33679 wl-ax11-lem8 33703 sbcrexgOLD 37875 pm13.193 39138 opeliun2xp 42639 |
Copyright terms: Public domain | W3C validator |