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

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

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