![]() |
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 2067. (Revised by BJ, 30-Dec-2020.) |
Ref | Expression |
---|---|
sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ2 2028 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦)) | |
2 | 1 | imbi1d 341 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
3 | 2 | albidv 1922 | . 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
4 | df-sb 2067 | . 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
5 | df-sb 2067 | . 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∀wal 1538 [wsb 2066 |
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 1912 ax-6 1970 ax-7 2010 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1781 df-sb 2067 |
This theorem is referenced by: sbequi 2086 sbcom3vv 2097 sbco2vv 2099 sbcom2 2160 drsb2 2256 sbco2v 2325 sbcom3 2504 sbco2 2509 sb10f 2525 sb8eulem 2591 eleq1ab 2710 cbvralsvwOLD 3315 cbvrexsvwOLD 3316 cbvralfwOLD 3319 cbvralf 3355 cbvralsv 3361 cbvrexsv 3362 cbvreuwOLD 3411 cbvreu 3423 cbvrabw 3466 cbvrab 3472 cbvreucsf 3940 cbvrabcsf 3941 ss2abdv 4060 cbvopab1g 5224 cbvmptf 5257 cbvmptfg 5258 cbviota 6505 sb8iota 6507 cbvriota 7382 tfis 7848 tfinds 7853 findes 7897 uzind4s 12899 wl-sbcom2d-lem1 36887 wl-sb8eut 36905 wl-dfclab 36921 sbeqi 37490 disjinfi 44349 2reu8i 46279 |
Copyright terms: Public domain | W3C validator |