Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbequ | Structured version Visualization version GIF version |
Description: Equality property for substitution, from Tarski's system. Used in proof of Theorem 9.7 in [Megill] p. 449 (p. 16 of the preprint). (Contributed by NM, 14-May-1993.) Revise df-sb 2070. (Revised by BJ, 30-Dec-2020.) |
Ref | Expression |
---|---|
sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ2 2033 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦)) | |
2 | 1 | imbi1d 344 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
3 | 2 | albidv 1921 | . 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
4 | df-sb 2070 | . 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
5 | df-sb 2070 | . 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
6 | 3, 4, 5 | 3bitr4g 316 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∀wal 1535 [wsb 2069 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1781 df-sb 2070 |
This theorem is referenced by: sbequi 2091 sbcom3vv 2106 sbco2vv 2108 sbcom2 2168 drsb2 2267 sbco2v 2352 sbcom3 2548 sbco2 2553 sb10f 2571 sb8eulem 2684 eleq1ab 2801 cbvralfw 3437 cbvralf 3439 cbvreuw 3443 cbvreu 3447 cbvralsvw 3467 cbvrexsvw 3468 cbvralsv 3469 cbvrexsv 3470 cbvrabw 3489 cbvrab 3490 cbvreucsf 3927 cbvrabcsf 3928 cbvopab1g 5140 cbvmptf 5165 cbvmptfg 5166 cbviota 6323 sb8iota 6325 cbvriota 7127 tfis 7569 tfinds 7574 findes 7612 uzind4s 12309 wl-sbcom2d-lem1 34810 wl-sb8eut 34828 wl-dfclab 34843 sbeqi 35452 disjinfi 41474 2reu8i 43332 |
Copyright terms: Public domain | W3C validator |