MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sbequ Structured version   Visualization version   GIF version

Theorem sbequ 2083
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.)
Assertion
Ref Expression
sbequ (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))

Proof of Theorem sbequ
Dummy variable 𝑢 is distinct from all other variables.
StepHypRef Expression
1 equequ2 2025 . . . 4 (𝑥 = 𝑦 → (𝑢 = 𝑥𝑢 = 𝑦))
21imbi1d 341 . . 3 (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑))))
32albidv 1920 . 2 (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑))))
4 df-sb 2065 . 2 ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)))
5 df-sb 2065 . 2 ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑)))
63, 4, 53bitr4g 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