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

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

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