![]() |
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 2403 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 → [𝑦 / 𝑧]𝜑)) | |
2 | sbequi 2403 | . . 3 ⊢ (𝑦 = 𝑥 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) | |
3 | 2 | equcoms 1993 | . 2 ⊢ (𝑥 = 𝑦 → ([𝑦 / 𝑧]𝜑 → [𝑥 / 𝑧]𝜑)) |
4 | 1, 3 | impbid 202 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 [wsb 1937 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-10 2059 ax-12 2087 ax-13 2282 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-ex 1745 df-nf 1750 df-sb 1938 |
This theorem is referenced by: drsb2 2406 sbcom3 2439 sbco2 2443 sbcom2 2473 sb10f 2484 sb8eu 2532 cbvralf 3195 cbvreu 3199 cbvralsv 3212 cbvrexsv 3213 cbvrab 3229 cbvreucsf 3600 cbvrabcsf 3601 sbss 4117 cbvopab1 4756 cbvmpt 4782 cbviota 5894 sb8iota 5896 cbvriota 6661 tfis 7096 tfinds 7101 findes 7138 uzind4s 11786 bj-cleljustab 32972 wl-sbcom2d-lem1 33472 wl-sb8eut 33489 wl-sbcom3 33502 sbeqi 34098 disjinfi 39694 |
Copyright terms: Public domain | W3C validator |