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 2239 | . 2 ⊢ (𝑥 = 𝑦 → (𝜑 → [𝑦 / 𝑥]𝜑)) | |
2 | sbequ2 2240 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑥]𝜑 → 𝜑)) | |
3 | 1, 2 | impbid 213 | 1 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ [𝑦 / 𝑥]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 [wsb 2060 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-12 2167 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 |
This theorem is referenced by: sbequ12r 2244 sbequ12a 2246 sb5 2267 sb8v 2364 sb8ev 2365 sbbib 2371 axc16ALT 2521 nfsb4t 2532 sbco2 2546 sb8 2552 sb8e 2553 sbal1 2565 sbal2 2566 clelab 2955 sbab 2957 nfabdw 2997 cbvralfw 3435 cbvralf 3437 cbvralsvw 3465 cbvrexsvw 3466 cbvralsv 3467 cbvrexsv 3468 cbvrabw 3487 cbvrab 3488 sbhypf 3550 mob2 3703 reu2 3713 reu6 3714 sbcralt 3852 sbcreu 3856 cbvrabcsfw 3921 cbvreucsf 3924 cbvrabcsf 3925 csbif 4518 cbvopab1 5130 cbvopab1g 5131 cbvopab1s 5133 cbvmptf 5156 cbvmptfg 5157 opelopabsb 5408 csbopab 5433 csbopabgALT 5434 opeliunxp 5612 ralxpf 5710 cbviotaw 6314 cbviota 6316 csbiota 6341 f1ossf1o 6882 cbvriotaw 7112 cbvriota 7116 csbriota 7118 onminex 7511 tfis 7558 findes 7601 abrexex2g 7654 opabex3d 7655 opabex3rd 7656 opabex3 7657 dfoprab4f 7743 uzind4s 12296 ac6sf2 30298 esumcvg 31244 wl-sb8t 34669 wl-sbalnae 34679 wl-ax11-lem8 34705 sbcrexgOLD 39260 scottabes 40455 pm13.193 40620 2reu8i 43189 opeliun2xp 44309 |
Copyright terms: Public domain | W3C validator |