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 2075. (Revised by BJ, 30-Dec-2020.) |
Ref | Expression |
---|---|
sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ2 2038 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦)) | |
2 | 1 | imbi1d 345 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
3 | 2 | albidv 1927 | . 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
4 | df-sb 2075 | . 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
5 | df-sb 2075 | . 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
6 | 3, 4, 5 | 3bitr4g 317 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 209 ∀wal 1540 [wsb 2074 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-sb 2075 |
This theorem is referenced by: sbequi 2094 sbcom3vv 2106 sbco2vv 2108 sbcom2 2169 drsb2 2267 sbco2v 2334 sbcom3 2510 sbco2 2515 sb10f 2532 sb8eulem 2599 eleq1ab 2718 cbvralfwOLD 3336 cbvralf 3338 cbvreuw 3342 cbvreu 3347 cbvralsvw 3368 cbvrexsvw 3369 cbvralsv 3370 cbvrexsv 3371 cbvrabw 3391 cbvrab 3392 cbvreucsf 3834 cbvrabcsf 3835 ss2abdv 3953 cbvopab1g 5104 cbvmptf 5129 cbvmptfg 5130 cbviota 6307 sb8iota 6309 cbvriota 7141 tfis 7588 tfinds 7593 findes 7633 uzind4s 12390 wl-sbcom2d-lem1 35337 wl-sb8eut 35355 wl-dfclab 35370 sbeqi 35940 disjinfi 42269 2reu8i 44138 |
Copyright terms: Public domain | W3C validator |