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 2068. (Revised by BJ, 30-Dec-2020.) |
Ref | Expression |
---|---|
sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ2 2029 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦)) | |
2 | 1 | imbi1d 342 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
3 | 2 | albidv 1923 | . 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
4 | df-sb 2068 | . 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
5 | df-sb 2068 | . 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1537 [wsb 2067 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-sb 2068 |
This theorem is referenced by: sbequi 2087 sbcom3vv 2098 sbco2vv 2100 sbcom2 2161 drsb2 2258 sbco2v 2327 sbcom3 2510 sbco2 2515 sb10f 2532 sb8eulem 2598 eleq1ab 2717 cbvralfwOLD 3369 cbvralf 3371 cbvreuwOLD 3377 cbvreu 3381 cbvralsvw 3402 cbvrexsvw 3403 cbvralsv 3404 cbvrexsv 3405 cbvrabw 3424 cbvrab 3425 cbvreucsf 3879 cbvrabcsf 3880 ss2abdv 3997 cbvopab1g 5150 cbvmptf 5183 cbvmptfg 5184 cbviota 6401 sb8iota 6403 cbvriota 7246 tfis 7701 tfinds 7706 findes 7749 uzind4s 12648 wl-sbcom2d-lem1 35714 wl-sb8eut 35732 wl-dfclab 35747 sbeqi 36317 disjinfi 42731 2reu8i 44605 |
Copyright terms: Public domain | W3C validator |