![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbequ | Structured version Visualization version 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, 14-May-1993.) |
Ref | Expression |
---|---|
sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequi 2451 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | |
2 | sbequi 2451 | . . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) | |
3 | 2 | equcoms 2067 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) |
4 | 1, 3 | impbid 204 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 [wsb 2011 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-10 2135 ax-12 2163 ax-13 2334 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-ex 1824 df-nf 1828 df-sb 2012 |
This theorem is referenced by: drsb2 2454 sbcom3 2487 sbco2 2492 sbcom2 2523 sbcom2OLD 2524 sb10f 2536 sb8eu 2635 cbvralf 3361 cbvreu 3365 cbvralsv 3378 cbvrexsv 3379 cbvrab 3395 cbvreucsf 3785 cbvrabcsf 3786 sbss 4305 cbvopab1 4959 cbvmpt 4984 cbviota 6104 sb8iota 6106 cbvriota 6893 tfis 7332 tfinds 7337 findes 7374 uzind4s 12054 bj-cleljustab 33422 wl-sbcom2d-lem1 33936 wl-sb8eut 33953 sbeqi 34590 cleljust2 38121 disjinfi 40303 2reu8i 42154 |
Copyright terms: Public domain | W3C validator |