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

Theorem sbequ 2093
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 2075. (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 2038 . . . 4 (𝑥 = 𝑦 → (𝑢 = 𝑥𝑢 = 𝑦))
21imbi1d 345 . . 3 (𝑥 = 𝑦 → ((𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)) ↔ (𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑))))
32albidv 1927 . 2 (𝑥 = 𝑦 → (∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)) ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑))))
4 df-sb 2075 . 2 ([𝑥 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑥 → ∀𝑧(𝑧 = 𝑢𝜑)))
5 df-sb 2075 . 2 ([𝑦 / 𝑧]𝜑 ↔ ∀𝑢(𝑢 = 𝑦 → ∀𝑧(𝑧 = 𝑢𝜑)))
63, 4, 53bitr4g 317 1 (𝑥 = 𝑦 → ([𝑥 / 𝑧]𝜑 ↔ [𝑦 / 𝑧]𝜑))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wal 1540  [wsb 2074
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1787  df-sb 2075
This theorem is referenced by:  sbequi  2094  sbcom3vv  2106  sbco2vv  2108  sbcom2  2169  drsb2  2267  sbco2v  2334  sbcom3  2510  sbco2  2515  sb10f  2532  sb8eulem  2599  eleq1ab  2718  cbvralfwOLD  3336  cbvralf  3338  cbvreuw  3342  cbvreu  3347  cbvralsvw  3368  cbvrexsvw  3369  cbvralsv  3370  cbvrexsv  3371  cbvrabw  3391  cbvrab  3392  cbvreucsf  3834  cbvrabcsf  3835  ss2abdv  3953  cbvopab1g  5104  cbvmptf  5129  cbvmptfg  5130  cbviota  6307  sb8iota  6309  cbvriota  7141  tfis  7588  tfinds  7593  findes  7633  uzind4s  12390  wl-sbcom2d-lem1  35337  wl-sb8eut  35355  wl-dfclab  35370  sbeqi  35940  disjinfi  42269  2reu8i  44138
  Copyright terms: Public domain W3C validator