| 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 2065. (Revised by BJ, 30-Dec-2020.) |
| Ref | Expression |
|---|---|
| sbequ | ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | equequ2 2025 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑢 = 𝑥 ↔ 𝑢 = 𝑦)) | |
| 2 | 1 | imbi1d 341 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
| 3 | 2 | albidv 1920 | . 2 ⊢ (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑)))) |
| 4 | df-sb 2065 | . 2 ⊢ ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
| 5 | df-sb 2065 | . 2 ⊢ ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢 → 𝜑))) | |
| 6 | 3, 4, 5 | 3bitr4g 314 | 1 ⊢ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 [wsb 2064 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 |
| This theorem is referenced by: sbequi 2084 sbcom3vv 2097 sbco2vv 2099 sbco4lem 2101 sbco4 2102 sbcom2 2173 drsb2 2266 sbco2v 2332 sbcom3 2511 sbco2 2516 sb10f 2532 sb8eulem 2598 eleq1ab 2716 cbvralsvwOLDOLD 3320 cbvrexsvwOLD 3321 cbvralf 3360 cbvralsv 3366 cbvrexsv 3367 cbvreuwOLD 3415 cbvreu 3428 cbvrabwOLD 3474 cbvrab 3479 cbvreucsf 3943 cbvrabcsf 3944 cbvopab1g 5218 cbvmptf 5251 cbvmptfg 5252 cbviota 6523 sb8iota 6525 cbvriota 7401 tfis 7876 tfinds 7881 findes 7922 uzind4s 12950 wl-sbcom2d-lem1 37560 wl-sb8eut 37579 wl-sb8eutv 37580 wl-dfclab 37597 sbeqi 38166 disjinfi 45197 2reu8i 47125 |
| Copyright terms: Public domain | W3C validator |